Dagstuhl Seminar 26052
Arithmetical and Modal mu-Calculi: Recent and Future Advances
( Jan 25 – Jan 30, 2026 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/26052
Organizers
- Bahareh Afshari (University of Gothenburg, SE)
- Juan P. Aguilera (TU Wien, AT)
- Dexter Kozen (Cornell University - Ithaca, US)
Contact
- Michael Gerke (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Dagstuhl Reports
As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.
- Upload (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
- Upload (Use personal credentials as created in DOOR to log in)
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
Please log in to DOOR to see more details.
- Bahareh Afshari (University of Gothenburg, SE) [dblp]
- Juan P. Aguilera (TU Wien, AT) [dblp]
- Florian Bruse (TU München - Garching, DE)
- Gianluca Curzi (University of Gothenburg, SE) [dblp]
- Anupam Das (University of Birmingham, GB) [dblp]
- Jacques Duparc (University of Lausanne, CH) [dblp]
- David Fernández-Duque (University of Barcelona, ES) [dblp]
- Rajeev P. Gore (Monash University - Clayton, AU) [dblp]
- Lide Grotenhuis (University of Amsterdam, NL) [dblp]
- Helle Hvid Hansen (University of Groningen, NL) [dblp]
- Gerhard Jäger (Universität Bern, CH)
- Johannes Kloibhofer (University of Amsterdam, NL)
- Cárolos Laméris (University of Groningen, NL)
- Martin Lange (Universität Kassel, DE) [dblp]
- Robert Lubarsky (Florida Atlantic University - Boca Raton, US) [dblp]
- Timothy Lyon (TU Dresden, DE)
- Stella Mahler (TU Wien, AT)
- Amaldev Manuel (Indian Institute of Technology Goa - Ponda, IN) [dblp]
- Guillaume Massas (Chapman University - Orange, US)
- Yoàv Montacute (University of Cambridge, GB & National Institute of Informatics, Tokyo, JP) [dblp]
- Damian Niwinski (University of Warsaw, PL) [dblp]
- Leonardo Pacheco (Institute of Science Tokyo, JP) [dblp]
- Michael Rathjen (University of Leeds, GB) [dblp]
- Reuben Rowe (Royal Holloway, University of London, GB) [dblp]
- Alexis Saurin (CNRS - Paris, FR) [dblp]
- Lutz Schröder (Universität Erlangen-Nürnberg, DE) [dblp]
- Michal Skrzypczak (University of Warsaw, PL) [dblp]
- Dominik Wehr (Universität Würzburg, DE)
- Keita Yokoyama (Tohoku University, JP) [dblp]
Classification
- Formal Languages and Automata Theory
- Logic in Computer Science
Keywords
- modal mu-calculus
- arithmetical mu-calculus
- cyclic proof
- provability logic
- infinite game
