FOR UP-TO-DATE INFORMATION REGARDING THE PROGRAMME, SEE THE CANVAS PAGES

Model checking has applications in a diversity of areas such as software and hardware verification (as expected), but also in

**2IMF35 --- Algorithms for Model Checking***"Given a model of a system, exhaustively and automatically check whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.*" (source: Wikipedia).Model checking has applications in a diversity of areas such as software and hardware verification (as expected), but also in

*planning*,*scheduling*,*mechanical engineering, business process mining*and*biology*. To understand the limitations of model checking, we study the mu-calculus, CTL* and some of its subsets such as LTL and CTL, from a computational viewpoint in these lectures. Among others, we treat the symbolic (fixed point based) algorithms for CTL, and fair CTL. The mu-calculus is discussed and its complexity is analysed. Transformations of the mu-calculus model checking problem to the frameworks of Boolean equation systems and Parity Games are addressed, combined with advanced algorithms for solving the latter artefacts.**Objectives**

After
taking this course, students are expected
to

- be capable of explaining the computational complexity of the model checking algorithms for (fair) CTL and the modal mu-calculus
- be capable of transforming (fair) CTL formulae to the modal mu-calculus
- be able to explain the role of OBDDs in symbolic model checking
- be capable of simplifying Parity Games and parameterised Boolean equation systems
- be able to reason about Parity Games
- be capable of explaining the computational complexity of the algorithms for solving Parity Games
- have the skills to manually execute the
algorithms for model checking (fair) CTL and the
modal mu-calculus
- be able to transform the problem of model checking to the modal mu-calculus to the problem of solving Boolean equation systems
- be able to transform the
problem of solving Boolean equation systems
to the problem of computing the winners in a Parity Game, and
*vice versa* - have the skills to manually solve (parameterised) Boolean equation systems and Parity Games using the algorithms presented in the course.