Some model theory for the modal μ-calculus: Syntactic characterisations of semantic properties

This paper contributes to the theory of the modal μ-calculus by proving some model-theoretic results. More in particular, we discuss a number of semantic properties pertaining to formulas of the modal μ-calculus. 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. The properties that we study all concern the way in which the meaning of a formula ξ in a model depends on the meaning of a single, fixed proposition letter p. For example, consider a formula ξ which is monotone in p; such a formula a formula ξ is called continuous (respectively, fully additive), if in addition it satisfies the property that, if ξ is true at a state s then there is a finite set (respectively, a singleton set) U such that ξ remains true at s 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. 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