Probabilistic and Stochastic Model Checking

Model checking is an automated formal verification technique whose main idea is to formally specify both the system specification and its properties (typically, by means of temporal logic) and automatically verify that such properties are satisfied (or to which extent they are). This course aims at presenting the fundamentals of model checking techniques for the verification of distributed and concurrent systems. Different classes of temporal logics will be introduced that rely on the use of semantic models to provide a logical framework for the analysis and verification of complex systems. The first part of the course will cover the fundamentals of qualitative model checking, while the second part of the course will cover the fundamentals of probabilistic model checking and its application to performance evaluation.