Evènement pour le groupe Séminaire Méthodes Formelles
|Date|| 2018-11-13 11:00-12:00|
|Titre||Complexity bounds for bisimulation equivalence in first-order grammars |
|Résumé||Following Géraud 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 Colin Stirling and Petr Jancar, 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 will cover some work in progress with Petr Jancar. Using a recent reformulation of the proofs for checking bisimulation equivalence as a black box, I will show 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 Petr Jancar a few years ago; this is the first known completeness result in this entire line of work. |
|Orateur||Sylvain Schmitz |
|Url||LSV, ENS Cachan |
Aucun document lié à cet événement.RetourRetour à l'index