A Characterization Theorem for the Alternation-Free Fragment of the Modal µ-Calculus
A Characterization Theorem for the Alternation-Free Fragment of the Modal µ-Calculus
复制标题
模态μ微积分无交替片段的表征定理
DOI：
10.1109/lics.2013.54
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
F. Zanasi
中科院分区：
文献类型：
--
作者：
Alessandro Facchini;Y. Venema;F. Zanasi
我们以 van Benthem 和 Janin-Walukiewicz 的风格为模态 μ 微积分的无交替片段提供了一个表征定理。为此，我们引入了标准一元二阶逻辑 (MSO) 的变体，我们将其称为有根据的一元二阶逻辑 (WFMSO)。当在树模型中解释时，WFMSO 的二阶量词范围涵盖相反有充分基础的子树的子集。论文的第一个主要结果表明，WFMSO 在树上的表达能力与弱 MSO 自动机的表达能力完全一致。使用这种自动机理论表征，我们表明，在所有过渡结构的类别上，WFMSO 的互模拟不变片段是模态 μ 演算的无交替片段。作为推论，我们发现逻辑 WFMSO 和 WMSO（弱单子二阶逻辑，其中二阶量化涉及有限子集）在表达能力上是无法比拟的。
We provide a characterization theorem, in the style of van Benthem and Janin-Walukiewicz, for the alternation-free fragment of the modal μ-calculus. For this purpose we introduce a variant of standard monadic second-order logic (MSO), which we call well-founded monadic second-order logic (WFMSO). When interpreted in a tree model, the second-order quantifiers of WFMSO range over subsets of conversely well-founded subtrees. The first main result of the paper states that the expressive power of WFMSO over trees exactly corresponds to that of weak MSO-automata. Using this automata-theoretic characterization, we then show that, over the class of all transition structures, the bisimulation-invariant fragment of WFMSO is the alternation-free fragment of the modal μ-calculus. As a corollary, we find that the logics WFMSO and WMSO (weak monadic second-order logic, where second-order quantification concerns finite subsets), are incomparable in expressive power.
DOI：
10.1016/j.apal.2009.04.002
发表时间：
2009
期刊：
20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)
影响因子：
--
作者：
A. Dawar;M. Otto
通讯作者：
M. Otto