Mu-calculi are logical systems for reasoning about inductive and co-inductive constructions. They link a number of important fields in mathematics and theoretical computer science: arithmetic, recursion theory, temporal and spatial logics, topology, infinite games, descriptive set theory, and automata theory. The purpose of this Dagstuhl Seminar is to bring together experts from these fields to discuss connections and encourage new avenues of interdisciplinary collaboration.

The modal mu-calculus is a decidable logic with high expressive power, able to simulate a broad collection of temporal and spatial logics of interest for applications. The contrast of high expressivity and low complexity makes its study challenging. Its proof theory, for instance, relies on ill-founded infinitary proofs and appeals to the determinacy of infinite games.

The arithmetical mu-calculus, although similar in spirit to the modal mu-calculus, is set apart by its undecidability and non-recursive expressive power. The language of the arithmetical mu-calculus is powerful enough to define winning strategies for infinite games in low levels of the Borel hierarchy, for example parity games, notably utilized for decidability proofs in automata theory (e.g., Rabin’s theorem). Moreover, results from reverse mathematics demonstrate that indeed such expressive power is crucial to these decidability proofs.

Various notable recent developments have motivated this Dagstuhl Seminar. These include topological developments in mu-calculus, non-classical generalizations of temporal and spatial logics, descriptive set theoretic considerations on the existence of winning strategies for infinite games, and decidability results for sophisticated automata.

Creative Commons BY 4.0

Bahareh Afshari, Juan P. Aguilera, and Dexter Kozen