Unboundedness and Downward Closures of Higher-Order Pushdown Automata

2015/07/13 by Matthew Hague, Hague, Matthew, Jonathan Kochems +3
Computer Science · #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1507.03304

openalex publication_date 2015/07/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

Related

• The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
• An approach to computing downward closures
• Computing downward closures for stacked counter automata
• Bounded treewidth, multiple context-free grammars, and downward closures
• Higher-Order Recursion Schemes and Collapsible Pushdown Automata:\n Logical Properties