Modal Fixpoint Logics: When Logic Meets Games, Automata and Topology
Alessandro Facchini & Damian Niwinski
Logic & Computation
Week Two - 14.00-15.30 - Level: A
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.