Alessandro Facchini & Damian Niwinski

Logic & Computation

Week Two - 14.00-15.30 - Level: A

Room: N9


The aim of the course is to give a first glimpse to this rich web of connections between logic, automata, topology and games, and to try reveal a bit of the whole beauty and complexity of the theory underlying the modal mu calculus, an extension of modal logic with fixpoints. More specifically:

  • We present the basic laws of the mu-calculus and explain its semantics in terms of parity games. We show how such games can shed light on the algorithmic aspect of the corresponding model-checking problem.
  • We explain the basic connections between monadic second order logic, mu-calculus and automata and show how we can use it to prove properties of the mu-calculus, like the finite model property and the Janin-Walukiewicz theorem (mu-calculus is the bisimulation invariant fragment of MSO).
  • We explain how topological hardness is often behind expressiveness results. In particular we show how the strictness of the fixpoint alternation hierarchy can be easily proved by a topological argument.
  • We introduce a quantitative extension of the modal mu-calculus for expressing properties of probabilistic transition systems, and show to which extents it is possible to extend the elegant mathematical theory of the standard mu calculus to this setting.