Equivalences of pushdown systems are hard

Abstract

Language equivalence of deterministic pushdown automata (DPDA) was shown to be decidable by Sénizergues (1997, 2001); Stirling (2002) then showed that the problem is primitive recursive. Sénizergues (1998, 2005) also generalized his proof to show decidability of bisimulation equivalence of (nondeterministic) PDA where ε-rules can be only deterministic and popping; this problem was shown to be nonelementary by Benedikt, Göller, Kiefer, and Murawski (2013), even for PDA with no ε-rules. Here we refine Stirling's analysis and show that DPDA equivalence is in TOWER, i.e., in the "least" nonelementary complexity class. The basic proof ideas remain the same but the presentation and the analysis are simplified, in particular by using a first-order term framework. The framework of (nondeterministic) first-order grammars, with term root-rewriting rules, is equivalent to the model of PDA with restricted ε-rules to which Sénizergues's decidability proof applies. We show that bisimulation equivalence is here Ackermann-hard, and thus not primitive recursive. © 2014 Springer-Verlag.