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