Bisimilarity of pushdown automata is nonelementary

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.

Authors

• Michael Benedikt
• Stefan Göller
• Stefan Kiefer
• Andrzej Murawski

Keywords

No keywords are indexed for this paper.