The Complexity of Games on Higher Order Pushdown Automata

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.

Cited by in corpus (5)

• Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
• Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
• Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
• Collapsible Pushdown Parity Games
• Annotated Stack Trees