Unboundedness and Downward Closures of Higher-Order Pushdown Automata

TL;DR

This paper proves the decidability of the diagonal problem for higher-order pushdown automata, enabling the construction of their downward closures and Parikh images, which are crucial for verifying complex higher-order programs.

Contribution

It establishes the decidability of the diagonal problem for HOPDA and enables the construction of downward closures and Parikh images, advancing verification techniques for higher-order programs.

Findings

Diagonal problem for HOPDA is decidable

Downward closures of accepted words can be constructed

Parikh images of HOPDA can be computed

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.