arXiv 1502.045782015-02-17cs.LO

The MSO+U theory of (N, <) is undecidable

Mikołaj Bojańczyk, Paweł Parys, Szymon Toruńczyk

备注：: 9 pages, with 2 figures

英文摘要：

We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

带无界量词的弱Mso

Weak Mso with the Unbounding Quantifier

本文引入了一类新的无限词语言，称之为极大正则语言，它是对$ω$ -正则语言类的扩充.这个类有两个等价的描述：自动机（一种确定性计数器自动机）和逻辑（带有边界量词的弱一元二阶逻辑）。给出了逻辑和自动机之间的有效转换。

2009-02-06cs.FLcs.LO

Weak MSO+U with Path Quantifiers over Infinite Trees

This paper shows that over infinite trees, satisfiability is decidable for weak monadic second-order logic extended by the unbounding quantifier U and quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees.

2014-04-29cs.LO

MSO+nabla is undecidable

This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying ``almost surely a branch π \in {0, 1}^w satisfies a formula ϕ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative probabilistic CTL, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+nabla is true in the full binary t…

2019-04-29cs.LO

递归方案、MSO逻辑与U量词

Recursion Schemes, the MSO Logic, and the U quantifier

本文证明了对递归方案生成的树，在MSO逻辑基础上增加受限的U量词（表示对任意大有限集为真）后，模型检验问题仍可判定，且该逻辑具有反射性和有效选择性质。

2020-02-17cs.LO

弱版本 MSO+U 的不可判定性

Undecidability of a weak version of MSO+U

本文证明在 $\omega$-词上扩展二阶谓词 $U_1$ 的 MSO 不可判定，并推论允许量化最终周期集合时 MSO 也不可判定。

2020-02-10cs.LO

Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable

We prove that the theory of Monadic Second-Order logic (MSO) of the infinite binary tree extended with qualitative path-measure quantifier is undecidable. This quantifier says that the set of infinite paths in the tree that satisfies some formula has Lebesgue-measure one. To do this we prove that the emptiness problem of qualitative universal parity tree automata is undecidable. Qualitative means that a run of a tree automaton is accepting if the set of paths in the run that satisfy the acceptance condition has Lebesgue-measure one.

2019-02-15cs.LO

更多相关论文收起更多论文

Undecidable First-Order Theories of Affine Geometries

Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation β, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of the class of expansions of (R^2,β) with just one unary predicate is not even arithmetical. We also define a natural and comprehe…

2013-12-25cs.LOmath.LO

Undecidable First-Order Theories of Affine Geometries

Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (β) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of monadic expansions of (R^2,β) is Π^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive c…

2012-08-24cs.CCcs.LOmath.LO

Succinctness of Order-Invariant Logics on Depth-Bounded Structures

We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on structures of bounded tree-depth. Order- invariance is undecidable in general and, thus, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on structures of bounded tree-depth, order-invariant FO has the same expressive power as FO. Our proof technique allows for a fine-grained analysis of the succinctness of this translation. We show that for every order-invariant FO sentence there exi…

2016-03-30cs.LO

Quantified CTL with imperfect information

Quantified CTL (QCTL) is a well-studied temporal logic that extends CTL with quantification over atomic propositions. It has recently come to the fore as a powerful intermediary framework to study logics for strategic reasoning. We extend it to include imperfect information by parameterising quantifiers with an observation that defines how well they observe the model, thus constraining their behaviour. We consider two different semantics, one related to the notion of no memory, the other to perfect recall. We study the expressiveness of our logic, and show that it coincides with MSO for the fi…

2018-09-03cs.LO

Expansions of MSO by cardinality relations

We study expansions of the Weak Monadic Second Order theory of (N,<) by cardinality relations, which are predicates R(X1,...,Xn) whose truth value depends only on the cardinality of the sets X1, ...,Xn. We first provide a (definable) criterion for definability of a cardinality relation in (N,<), and use it to prove that for every cardinality relation R which is not definable in (N,<), there exists a unary cardinality relation which is definable in (N,<,R) and not in (N,<). These results resemble Muchnik and Michaux-Villemaire theorems for Presburger Arithmetic. We prove then that + and x are d…

2013-12-04cs.LOmath.LO

元胞自动机轨道上的 FO 逻辑等价于 MSO 逻辑

FO logic on cellular automata orbits equals MSO logic

本文将经典元胞自动机扩展至任意标记图，证明其轨道上的 FO 逻辑等价于 MSO 逻辑，并据此推导出模型检测与可满足性的不可判定性结论及具体公式实例。

2024-04-25cs.DMcs.LOmath.DS

基于拉宾-莫斯科维茨指数的广义量词

Generalised Quantifiers Based on Rabin-Mostowski Index

本文提出基于拉宾-莫斯科维茨指数的广义量词，研究其在ω-词和无限树中的表达力和可判定性，发现两者在逻辑特性上有显著差异。

2026-01-08cs.FLcs.LO

与Parikh和Muller的可判定（计）数：将Presburger算术添加到树可解释结构上的单子二阶逻辑中

Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures

提出$ω$MSO$\Join$BAPA逻辑，通过Parikh-Muller树自动机证明其在树可解释结构上的可满足性可判定，并推广至带高级计数的双变量逻辑与$μ$-演算。

2023-11-23cs.FLcs.LO

Computation Tree Logic for Synchronization Properties

We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is i…

2016-05-24cs.FLcs.LO