Bisimilarity of Pushdown Automata is Nonelementary
Michael Benedikt, Stefan Göller, Stefan Kiefer, Andrzej S. Murawski · 2013
Given two pushdown automata, the bisimilarity problem asks whether the infinite transition systems they induce are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the best previously known lower bound for this problem. Our lower bound result holds for normed pushdown automata as well.