Bisimilarity of Pushdown Automata is Nonelementary.

Michael Benedikt, Stefan Gller, Stefan Kiefer, Andrzej S. Murawski

Browse the full LICS paper archive.