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 µ-calculus model checking over graphs given by n-HPDA is n-exptime complete.

• Type: Journal
• Year: 2007
• Where: CORR
• Authors: Thierry Cachat, Igor Walukiewicz
• Keywords: CORR 2007, Education, HPDA, N-exptime Lower Bound, Reachability Game