一句话：为模态 μ-演算的若干语义性质给出对应语法片段，并用自动机变换证明其可判定性。
本文研究模态 μ-演算公式相对于某个固定命题变元 p 的语义性质，例如单调性、连续性与完全可加性等；这些性质分别对应树模型中单点集、有限集、有限分支子树、无无穷路径子树（noetherian）和分支等特殊子集。作者为每种性质构造一个语法片段，证明公式具有该性质当且仅当它等价于该片段中的公式，且等价公式可有效求出。证明采用自动机论方法：语法片段由模态自动机上的简单变换诱导。由此推论，可在初等时间内判定给定 μ-公式是否具有相应性质，并推进模态自动机的模型论。
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.
@article{paperbot428,
title = {Some model theory for the modal $\mu$-calculus: syntactic characterisations of semantic properties},
author = {Gaëlle Fontaine and Yde Venema},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:14)2018}
}