Modal fixpoint logics

Modal fixpoint logics constitute a research field of considerable interest, not only because of their many applications, but also because of their rich logical/mathematical theory. Systems such as LTL, PDL, CTL, and the modal mu-calculus, originate from computer science, and are for instance applied in the theory of program specification and verification. The richness of their theory stems from deep connections with various fields in logic, mathematics, and theoretical computer science, such as lattices and universal (co-)algebra, modal logic, automata, and game theory.

Large areas of the theory of modal fixpoint logics, in particular the connection with the theory of automata and games, have been intensively investigated and are by now are well understood. Nevertheless, there are still many aspects that are less explored. This applies in particular to the model theory, intended as the study of a logic as a function of classes of models, the proof theory, the algebraic logic, duality theory in the spirit of Stone/Priestley duality, and the relation to the theory of ordered sets as grounding the concept of "least fixpoint".


The aim of the workshop is to bring together researchers from various backgrounds, in particular, computer scientists and pure logicians, who share an interest in the area. The invited talks together will represent an overview of the richness of the theory of modal fixpoint logics.