Modal fixpoint logics constitute a research field of considerable interest, not only because of its many applications in computer science, but also because of its rich mathematical theory, which features connections with fields as diverse as lattice theory, automata theory, and universal coalgebra.

In this talk I discuss so-called flat fixpoint logics. These arise by adding fixpoint connectives to a basic (poly-)modal languages. The semantics of these fixpoint connectives is defined using a least (or greatest) fixpoint of some modal formula. Examples of such logics, that are all included in the alternation-free fragment of the modal mu-calculus, are LTL and CTL.

After providing the basic definitions I will first discuss the question when such fixpoint connectives are constructive, that is, the fixpoint is approximated in finitely many rounds. I will then turn to the main topic of the talk: the axiomatics of flat modal fixpoint logics. I will present a general completeness theorem, and give a sketch of the proof.