Evènement pour le groupe Séminaire Méthodes Formelles

Date 2018-11-13  11:00-12:00
TitreComplexity 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. 
OrateurSylvain Schmitz 
UrlLSV, ENS Cachan 

Aucun document lié à cet événement.

Retour à l'index