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
Type of course
Assessment criteria
Final exam.
Bibliography
- Bradfield, J., Stirling C.: Modal Logic and Mu-Calculi. In: J. Bergstra, et al.: Handbook of Process Algebra Elsevier, North-Holland: 293-332 (2001)
- Graedel E., Thomas W., Wilke T. (Eds.): Automata, Logics, and Infinite Games. LNCS 2500, Springer-Verlag Berlin Heidelberg (2002)
- Janin D., Walukiewicz I.: Automata for the ?-Calculus and Related Results. MFCS ?95: 552-562 (1996)
- Wilke T.: Alternating Tree Automata, Parity Games, and Modal ?-Calculus. Bul. Belg. Math. Soc. 8(2): 359?391 (2001)
- Venema Y.: Lectures on the Modal mu-Calculus (2008) [http://staff.science.uva.nl/~yde/teaching/ml/mu/mu2008.pdf]
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: