Expressiveness of Monadic Second-Order Logics on Infinite Trees of Arbitrary Branching Degree
Expressiveness of Monadic Second-Order Logics on Infinite Trees of Arbitrary Branching Degree
复制标题
任意分支度无限树上的一元二阶逻辑的表达性
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Y. Venema
中科院分区：
文献类型：
--
作者：
Fabio Zanasi;J. V. Benthem;Alessandro Facchini;Helle Hvid Hansen;Benedikt Löwe;Y. Venema
本文利用自动机研究了无限树上一元二阶逻辑（MSO）变体的表达能力。我们特别感兴趣的是弱MSO和成立良好的MSO，其中二阶量词分别在有限集和成立良好的树的子集上。在有限分支树上，弱MSO和有充分基础的MSO具有相同的表达能力，并且都严格弱于MSO。相关的自动机类（称为弱mso自动机）是表征mso表达性的类的限制。我们证明，在任意分支度的树上，弱MSO自动机表征了建立良好的MSO的表达能力，这是弱MSO无法比拟的。事实上，在这种广义的情况下，弱MSO给出了树的“水平维度”的属性，这不能用MSO或有充分根据的MSO公式来描述。与Janin和Walukiewicz对MSO和模态μ-演算的结果类似，这提出了模态逻辑捕获良好MSO和弱MSO的双模拟不变片段的问题。我们证明了模态μ微积分的无交替片段和建立良好的MSO的双模拟不变片段在任意分支度的树上具有相同的表达能力。我们提出了弱MSO模双模拟在MSO和有充分根据的MSO内部崩溃的猜想。
In this thesis we study the expressive power of variants of monadic second-order logic (MSO) on infinite trees by means of automata. In particular we are interested in weak MSO and well-founded MSO, where the second-order quantifiers range respectively over finite sets and over subsets of well-founded trees. On finitely branching trees, weak and well-founded MSO have the same expressive power and are both strictly weaker than MSO. The associated class of automata (called weak MSO-automata) is a restriction of the class characterizing MSO-expressivity. We show that, on trees with arbitrary branching degree, weak MSO-automata characterize the expressive power of well-founded MSO, which turns out to be incomparable with weak MSO. Indeed, in this generalized setting, weak MSO gives an account of properties of the ‘horizontal dimension’ of trees, which cannot be described by means of MSO or well-founded MSO formulae. In analogy with the result of Janin and Walukiewicz for MSO and the modal μ-calculus, this raises the issue of which modal logic captures the bisimulation-invariant fragment of well-founded MSO and weak MSO. We show that the alternation-free fragment of the modal μ-calculus and the bisimulation-invariant fragment of well-founded MSO have the same expressive power on trees of arbitrary branching degree. We motivate the conjecture that weak MSO modulo bisimulation collapses inside MSO and well-founded MSO.