Weak MSO+U with path quantifiers over infinite trees

DOI10.1007/978-3-662-43951-7_4MaRDI QIDQ5167825zbMATH OpenOpenAlexFDO

Authors Mikołaj Bojańczyk

Publication date 1 July 2014

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1404.7278

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05)

Abstract: 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.

Recommendations

• Weak \(\text{MSO}+U\) over infinite trees
• On the decidability of MSO+U on infinite trees
• scientific article; zbMATH DE number 6829362
• Monadic second order finite satisfiability and unbounded tree-width
• Thin MSO with a probabilistic path quantifier

Cited in

(21)

• Parameterized linear temporal logics meet costs: still not costlier than LTL
• Weak \(\text{MSO}+U\) over infinite trees
• Delay games with WMSO+U winning conditions
• Delay games with WMSO+U winning conditions
• Recursion schemes and the WMSO+U logic
• New algorithm for weak monadic second-order logic on inductive structures
• Thin MSO with a probabilistic path quantifier
• On a fragment of AMSO and tiling systems
• An Extension of Muchnik's Theorem
• Trees over infinite structures and path logics with synchronization
• Parameterized linear temporal logics meet costs: still not costlier than LTL
• Recursion schemes, the MSO logic, and the \textsf{U} quantifier
• On the decidability of MSO+U on infinite trees
• Undecidability of a weak version of MSO+U
• Forcing MSO on infinite words in weak MSO
• Monadic second order finite satisfiability and unbounded tree-width
• Computer Science Logic
• Church synthesis on register automata over linearly ordered data domains
• Extending the WMSO+U logic with quantification over tuples
• Church synthesis on register automata over linearly ordered data domains
• A dichotomy theorem for ordinal ranks in MSO

This page was built for publication: Weak MSO+U with path quantifiers over infinite trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5167825)