The diagonal problem for higher-order recursion schemes is decidable

DOI10.1145/2933575.2934527zbMATH Open1401.68158arXiv1605.00371OpenAlexW2346985033MaRDI QIDQ4635865FDOQ4635865

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)

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.

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

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

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)

Cited In (13)

• Recursion schemes and the WMSO+U logic
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• Title not available (Why is that?)
• The Complexity of the Diagonal Problem for Recursion Schemes
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• 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)