摘要：We show that bisimulation equivalence of order-two pushdown automata is undecidable. Moreover, we study the lower order problem of higher-order pushdown automata, which asks, given an order-k pushdown automaton and some k' = 2 even when the input k-PDA is deterministic and real-time.
