Unboundedness and Downward Closures of Higher-Order Pushdown Automata

We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zet-zsche 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 rôle in verifying concur-rent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.