The Complexity of Games on Higher Order Pushdown Automata

TL;DR

This paper establishes the computational complexity of deciding winners in reachability games on higher order pushdown automata, showing it is n-EXPTIME complete, which matches existing upper bounds and impacts mu-calculus model checking.

Contribution

It proves an n-EXPTIME lower bound for reachability games on n-level HPDA, matching the known upper bound and clarifying the complexity of related model checking tasks.

Findings

Deciding the winner is n-EXPTIME complete for n-HPDA.

The complexity bound matches the known upper bound.

Implications for mu-calculus model checking on n-HPDA graphs.

Abstract

We prove an n-EXPTIME lower bound for the problem of deciding the winner in a reachability game on Higher Order Pushdown Automata (HPDA) of level n. This bound matches the known upper bound for parity games on HPDA. As a consequence the mu-calculus model checking over graphs given by n-HPDA is n-EXPTIME complete.