Decidability results for the boundedness problem

DOI10.2168/LMCS-10(3:2)2014MaRDI QIDQ2878748zbMATH OpenOpenAlexFDO

Authors Achim Blumensath, Martin Otto, Mark Weyer

Publication date 5 September 2014

Published in Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

boundednessfixed pointsmonadic second-order logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25)

Abstract: We prove decidability of the boundedness problem for monadic least fixed-point recursion based on positive monadic second-order (MSO) formulae over trees. Given an MSO-formula phi(X,x) that is positive in X, it is decidable whether the fixed-point recursion based on phi is spurious over the class of all trees in the sense that there is some uniform finite bound for the number of iterations phi takes to reach its least fixed point, uniformly across all trees. We also identify the exact complexity of this problem. The proof uses automata-theoretic techniques. This key result extends, by means of model-theoretic interpretations, to show decidability of the boundedness problem for MSO and guarded second-order logic (GSO) over the classes of structures of fixed finite tree-width. Further model-theoretic transfer arguments allow us to derive major known decidability results for boundedness for fragments of first-order logic as well as new ones.

Recommendations

• Boundedness of Monadic FO over Acyclic Structures
• The complexity of boundedness for guarded logics
• Monadic second order finite satisfiability and unbounded tree-width
• Guarded fixed point logics and the monadic theory of countable trees.
• An Extension of Muchnik's Theorem

Cited in

(17)

• A unified approach to boundedness properties in MSO
• scientific article; zbMATH DE number 7724207 (Why is no real title available?)
• Some new decidability results on positive and negative set constraints
• Lower bounds for some decision problems over \(C\)
• scientific article; zbMATH DE number 1948184 (Why is no real title available?)
• Decidability, partial decidability and sharpness relation for L-subsets
• scientific article; zbMATH DE number 7471708 (Why is no real title available?)
• Resolution of the uniform lower bound problem in constructive analysis
• On the complexity of decision using destinies in \(H\)-bounded structures
• Boundedness of Monadic FO over Acyclic Structures
• On undecidability bounds for matrix decision problems
• scientific article; zbMATH DE number 7104937 (Why is no real title available?)
• scientific article; zbMATH DE number 1089735 (Why is no real title available?)
• scientific article; zbMATH DE number 7561597 (Why is no real title available?)
• A more general theory of static approximations for conjunctive queries
• A more general theory of static approximations for conjunctive queries
• Trading bounds for memory in games with counters

This page was built for publication: Decidability results for the boundedness problem

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