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

separability problemhigher-order recursion schemesdownward closurediagonal problemhigher-order OI grammars

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Decidability of theories and sets of sentences (03B25) 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

(13)

• Recursion schemes and the WMSO+U logic
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• scientific article; zbMATH DE number 7199579 (Why is no real title available?)
• The Complexity of the Diagonal Problem for Recursion Schemes
• scientific article; zbMATH DE number 7204383 (Why is no real title available?)
• Unboundedness problems for machines with reversal-bounded counters
• Cost Automata, Safe Schemes, and Downward Closures
• Existential Definability over the Subword Ordering
• A type system describing unboundedness
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• scientific article; zbMATH DE number 7526052 (Why is no real title available?)
• Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
• Typed Lambda Calculi and Applications

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)