Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Optimizing Buechi Automata Inclusion Checking with Subsumption Preorders
du groupe Modélisation et Verification

Date 2012-01-19  11:30-12:30
TitreOptimizing Buechi Automata Inclusion Checking with Subsumption Preorders  
RésuméInclusion checking is a central algorithmic problem in the theory of automata, with important applications, e.g., in formal methods. The problem is PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected. We optimize the so-called Ramsey-based approach to inclusion checking. In this approach, one explores a semigroup of exponential size for a counter-example to inclusion. The exploration starts from a small set of generators, and all elements of the semigroup are progressively computed by composition. On the way, a test operation is used to check for counter-examples. The exploration stops if a counter-example is found; otherwise, all elements are generated. Clearly, exhaustive exploration of the semigroup is in general infeasible, due to its exponential size. We show how coarse simulation-based subsumption preorders between elements of the semigroup can be designed, allowing one to prune away significant parts of the search space. Subsumption allows us to solve inclusion checking for automata with thousand states, which was unthinkable before. More details can be found on http://www.languageinclusion.org/. 
Lieu076 
OrateurLorenzo Clemente 
Emaillorentzo.clemente@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index