Séminaire de l'équipe Méthodes Formelles, 11am, November 13, 2018, LaBRI, Bordeaux, France.
Following
Sénizergues' seminal results twenty years ago on the decidability of language equivalence of deterministic pushdown automata and of (weak) bisimilation equivalence of (epsilon-popping) pushshdown automata, several works have attempted to provide complexity bounds for these problems. For instance, some significant simplifications over the original proofs were provided by
Stirling and
Jančar, using in particular the formalism of first-order grammars instead of pushdown automata, and resulting in Tower upper bounds for the language equivalence problem in deterministic systems. But no complexity bounds were known for the bisimulation equivalence problem. In this talk, I covered some work in progress with
Petr Jančar. Using a recent reformulation of the proofs for checking bisimulation equivalence as a black box, I showed how to provide Ackermannian upper bounds for the crucial step, which is the computation of a so-called `candidate basis'. This entails that the decision problem itself is Ackermann-complete, thanks to a lower bound proven by
Jančar a few years ago; this is the first completeness result in this line of work.