An introduction to the modal mu-calculus 1000-2M12MU

As a mathematical framework to reason about fixpoints in modal logic, the modal mu-calculus constitutes a "meta" formal system for many logics used in computer science, like LTL, PDL and CTL. It is indeed weaker than second order logics, but sustains enough expressibility for many applications, in particular in program synthesis and verification. Moreover, it is also beautifully connected with the theory of automata, since modal mu-calculus is in fact equivalent to alternating automata.
Modal mu-calculus forms a research field of considerable interest, because of the richness of its powerful, although simple, mathematical theory which establishes deep connections particularly with logic, automata and game theory.

• During the classes, at least the following topics will be discussed
- modal mu-calculus: syntax, and equivalence between standard fixpoint semantic and game-theoretical semantic
- relation with other modal fixpoint logics, like PDL, CTL, CTL*
- non-deterministic and alternating automata, and the (corresponding) simulation theorem
- finite model property, decidability and interpolation for the modal mu-calculus
- Janin-Walukiewicz characterization theorem for MSO and the modal mu-calculus
- strictness of the fixpoint alternation hierarchy