Monadic second order finite satisfiability and unbounded tree-width

DOI10.4230/LIPICS.CSL.2016.13MaRDI QIDQ5278399zbMATH OpenOpenAlexFDO

Authors Helmut Veith, Florian Zuleger, Tomer Kotek

Publication date 19 July 2017

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

zbMATH Keywords

finite decidabilitymonadic second-order logic MSOtwo-variable fragment with counting C2unbounded tree-widthWS1S with cardinality constraints

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Model theory of finite structures (03C13)

Abstract: The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable: Input: (i) A monadic second order logic sentence $alpha$, and (ii) a sentence $$ in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of $alpha$ and $$ may intersect. Output: Is there a finite structure which satisfies $$ such that the restriction of the structure to the vocabulary of $alpha$ has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form $|X_1|+cdots+|X_r|<|Y_1|+cdots+|Y_s|$, where the $X_i$ and $Y_j$ are monadic second order variables. We prove the decidability of a similar extension of WS1S.

Recommendations

• The monadic second-order logic of graphs, II: Infinite graphs of bounded width
• scientific article; zbMATH DE number 2038747
• Weak \(\text{MSO}+U\) over infinite trees
• Weak MSO+U with path quantifiers over infinite trees
• On the parameterized intractability of monadic second-order logic

Cited in

(14)

• Branch-width, parse trees, and monadic second-order logic for matroids.
• scientific article; zbMATH DE number 1670771 (Why is no real title available?)
• Decidability results for the boundedness problem
• Weak \(\text{MSO}+U\) over infinite trees
• Expressing cardinality quantifiers in monadic second-order logic over trees
• Fly-automata for checking monadic second-order properties of graphs of bounded tree-width
• Bounded Second-Order Unification Is NP-Complete
• New algorithm for weak monadic second-order logic on inductive structures
• scientific article; zbMATH DE number 2038747 (Why is no real title available?)
• Weak MSO+U with path quantifiers over infinite trees
• Computer Science Logic
• Boundedness of Monadic FO over Acyclic Structures
• On the completeness and the decidability of strictly monadic second‐order logic
• Decidable (ac)counting with Parikh and Muller: adding Presburger arithmetic to monadic second-order logic over tree-interpretable structures

This page was built for publication: Monadic second order finite satisfiability and unbounded tree-width

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