The diagonal problem for higher-order recursion schemes is decidable

DOI10.1145/2933575.2934527MaRDI QIDQ4635865zbMATH OpenOpenAlexFDO

Authors Lorenzo Clemente, Paweł Parys, S. Salvati, Igor Walukiewicz

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

diagonal problemdownward closurehigher-order OI grammarshigher-order recursion schemesseparability problem

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42) Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.

Recommendations

• The Complexity of the Diagonal Problem for Recursion Schemes
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Unboundedness and downward closures of higher-order pushdown automata
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 1670473

Cited in

(23)

• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
• Recursion schemes and the WMSO+U logic
• A type system describing unboundedness
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• Intersection types for unboundedness problems
• Recursion schemes, the MSO logic, and the \textsf{U} quantifier
• scientific article; zbMATH DE number 7204383 (Why is no real title available?)
• The Complexity of the Diagonal Problem for Recursion Schemes
• Typed Lambda Calculi and Applications
• Cost Automata, Safe Schemes, and Downward Closures
• Unboundedness problems for machines with reversal-bounded counters
• Existential Definability over the Subword Ordering
• Timed games and deterministic separability
• Cost automata, safe schemes, and downward closures
• Size-preserving translations from order-(n+1) word grammars to order-n tree grammars
• Extending the WMSO+U logic with quantification over tuples
• Directed regular and context-free languages
• Priority downward closures
• Slice closures of indexed languages and word equations with counting constraints
• Verifying unboundedness via amalgamation
• Deterministic and game separability for regular languages of infinite trees
• Higher-order model checking step by step

This page was built for publication: The diagonal problem for higher-order recursion schemes is decidable

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