Yde Venema: Some model theory of the modal μ-calculus

The modal μ-calculus, an extension of basic modal logic with least and greatest fixpoint operators, has its roots in computer science, where it serves to unify and provide a foundation to various specification languages for programs and reactive systems. Besides this important role in formal verification, it has become increasingly clear over the years that the formalism also has a rich and beautiful meta-theory, and deserves a place in “pure” (mathematical) logic as well as in computer science.

In the talk we will discuss some model theory of the modal μ-calculus, focussing on a number of semantic properties that are of specific interest in the setting of modal fixpoint logic.

For example, call a formula ξ continuous in a proposition letter p if the map that represents the dependency of ξ on p is Scott continuous; as we will discuss, this is linked to the question whether the least fixpoint associated with this map can reached after \omega many approximations. An equivalent characterization of Scott continuity requires that if ξ is true at a certain state then there is a finite set U such that ξ remains true at the state if we restrict the interpretation of p to the set U.

Each of the properties that we consider is, in a similar way, associated with one of the following special kinds of subset of a tree model: singletons, finite sets, finitely branching subtrees, noetherian subtrees (i.e., without infinite paths), and branches. For each of these properties we provide a corresponding syntactic fragment, in the sense that a formula ξ has the given property iff it is equivalent to a formula ξ' in the corresponding fragment. Since this formula ξ' will always be effectively obtainable from ξ, as a corollary, for each of the properties under discussion, we prove that it is decidable in elementary time whether a given μ-calculus formula has the property or not.

Our proofs for these characterization results will be automata-theoretic in nature; we will see that the effectively defined maps on formulas are in fact induced by rather simple transformations on modal automata. Thus our results can also be seen as a contribution to the model theory of modal automata.

Finally, we will link these results with expressive completeness results. Where Janin and Walukiewicz identified the modal μ-calculus as the bisimulation invariant fragment of monadic second-order logic (MSO), I will mention similar results for weak MSO on the one hand, and for PDL and the alternation-free fragment of the modal μ-calculus on the other.

The talk is largely based on joint work with Gaelle Fontaine.