模态$μ$-演算的一些模型理论：语法特征化语义属性
摘要：对模态μ-演算理论做出了一些模型论的贡献。更具体地说，我们讨论了与模态μ-演算公式有关的一些语义性质。对于每个属性，我们提供了一个相应的语法片段，即当一个μ-公式ξ具有给定属性时，它等价于相应片段中的一个公式ξ'。作为推论，对于讨论的每个属性，我们证明了在基本时间内判断一个给定的μ-演算公式是否具有该属性是可判定的。我们研究的属性都涉及到模型中公式ξ的含义如何依赖于单个的、固定的命题符p的含义。例如，考虑一个在p上单调的公式ξ；这样一个公式ξ称为连续的（分别完全可加的），如果除此之外还满足以下性质：如果在状态s上公式ξ为真，则存在一个有限集合（分别为一个单元素集）U，使得当我们将p的解释限制在集合U上时，公式ξ仍在s上为真。我们考虑的每个属性都以下列特殊的树模型的子集之一相关联：单元素集，有限集，有限分支子树，无超限路径子树和枝。我们关于这些描述结果的证明将是自动机理论性质的；我们将看到，所定义的对公式的有效映射实际上是由模态自动机上的相当简单的变换引发的。因此我们的结果也可以看作是模态自动机的模型理论方面的一个贡献。
作者：Ga"elle Fontaine and Yde Venema
论文ID：1801.05994
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22