Reference:

Michael Benedikt, Stefan Göller, Stefan Kiefer, and Andrzej S. Murawski. Bisimilarity of pushdown automata is nonelementary. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 488–498, New Orleans, Louisiana, USA, 2013.

Abstract:

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.

Suggested BibTeX entry:

@inproceedings{13BGKM:lics,
    address = {New Orleans, Louisiana, USA},
    author = {Michael Benedikt and Stefan G\"{o}ller and Stefan Kiefer and Andrzej S. Murawski},
    booktitle = {Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
    pages = {488--498},
    title = {Bisimilarity of Pushdown Automata is Nonelementary},
    year = {2013}
}