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.
Paper Prompts
Sign up for free to create and run prompts on this paper using GPT-5.
Top Community Prompts
Collections
Sign up for free to add this paper to one or more collections.