Some model theory for the modal $\mu$-calculus: syntactic characterisations of semantic properties

This paper contributes to the theory of the modal $\mu$-calculus by provingsome model-theoretic results. More in particular, we discuss a number ofsemantic properties pertaining to formulas of the modal $\mu$-calculus. Foreach of these properties we provide a corresponding syntactic fragment, in thesense that a $\mu$-formula $\xi$ has the given property iff it is equivalent toa formula $\xi'$ in the corresponding fragment. Since this formula $\xi'$ willalways be effectively obtainable from $\xi$, as a corollary, for each of theproperties under discussion, we prove that it is decidable in elementary timewhether a given $\mu$-calculus formula has the property or not. The properties that we study all concern the way in which the meaning of aformula $\xi$ in a model depends on the meaning of a single, fixed propositionletter $p$. For example, consider a formula $\xi$ which is monotone in $p$;such a formula a formula $\xi$ is called continuous (respectively, fullyadditive), if in addition it satisfies the property that, if $\xi$ is true at astate $s$ then there is a finite set (respectively, a singleton set) $U$ suchthat $\xi$ remains true at $s$ if we restrict the interpretation of $p$ to theset $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 innature; we will see that the effectively defined maps on formulas are in factinduced by rather simple transformations on modal automata. Thus our resultscan also be seen as a contribution to the model theory of modal automata