模态 μ-演算的若干模型论：语义性质的语法刻画

本文通过证明若干模型论结果，对模态 μ-演算理论做出贡献。更具体地，我们讨论涉及模态 μ-演算公式的若干语义性质。对这些性质中的每一个，我们给出相应的语法片段，其意义在于：μ-公式 $\xi$ 具有给定性质当且仅当它等价于相应片段中的公式 $\xi'$。由于该公式 $\xi'$ 总能从 $\xi$ 有效获得，作为推论，对我们所讨论的每一性质，我们证明在初等时间内可判定给定 μ-演算公式是否具有该性质。我们所研究的性质均关乎公式 $\xi$ 在模型中的含义如何依赖于单个固定命题字母 $p$ 的含义。例如，考虑关于 $p$ 单调的公式 $\xi$；若此外满足如下性质：若 $\xi$ 在状态 $s$ 为真，则存在有限集（分别为单点集）$U$ 使得将 $p$ 的解释限制于集 $U$ 时 $\xi$ 在 $s$ 仍为真，则称此类公式 $\xi$ 为连续（分别为完全可加）。我们所考虑的每一性质都以类似方式关联于树模型下列特殊子集之一：单点集、有限集、有限分支子树、诺特子树（即无无限路径者）与分支。我们对这些刻画结果的证明本质上是自动机论的；我们将看到，公式上的有效定义映射事实上由模态自动机上的相当简单变换所诱导。因此，我们的结果也可视为对模态自动机模型论的贡献。