10.23638/LMCS-14(1:14)2018
Fontaine, Gaëlle
Gaëlle
Fontaine
Venema, Yde
Yde
Venema
Some model theory for the modal $\mu$-calculus: syntactic
characterisations of semantic properties
episciences.org
2018
Computer Science - Logic in Computer Science
F.4.1
contact@episciences.org
episciences.org
2018-01-22T15:40:03+01:00
2018-02-06T09:28:12+01:00
2018-02-06
eng
Journal article
https://lmcs.episciences.org/4225
arXiv:1801.05994
1860-5974
PDF
1
Logical Methods in Computer Science ; Volume 14, Issue 1 ; 1860-5974
This paper contributes to the theory of the modal $\mu$-calculus by proving
some model-theoretic results. More in particular, we discuss a number of
semantic properties pertaining to formulas of the modal $\mu$-calculus. For
each of these properties we provide a corresponding syntactic fragment, in the
sense that a $\mu$-formula $\xi$ has the given property iff it is equivalent to
a formula $\xi'$ in the corresponding fragment. Since this formula $\xi'$ will
always be effectively obtainable from $\xi$, as a corollary, for each of the
properties under discussion, we prove that it is decidable in elementary time
whether a given $\mu$-calculus formula has the property or not.
The properties that we study all concern the way in which the meaning of a
formula $\xi$ in a model depends on the meaning of a single, fixed proposition
letter $p$. For example, consider a formula $\xi$ which is monotone in $p$;
such a formula a formula $\xi$ is called continuous (respectively, fully
additive), if in addition it satisfies the property that, if $\xi$ is true at a
state $s$ then there is a finite set (respectively, a singleton set) $U$ such
that $\xi$ 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.