Description
Date depot: 28 mars 2019
Titre: Algorithmique des ω-automates
Directeur de thèse:
Alexandre DURET-LUTZ (LRE)
Encadrant :
Adrien POMMELLET (LRE)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé:
Les ω-automates sont des automates qui reconnaissent des mots infinis.Comme ces automates ont un nombre fini d'états, ils utilisent une*condition d'acceptation* pour décider quels chemins sontacceptants ou rejetants. Des conditions d'acceptation classiques sontconnues sous le nom de conditions de Büchi, de Rabin, de Streett, deMuller, de parité, etc. Elle correspondent à des contraintes sur desensembles d'états qui doivent être visités infiniment souvent, oufiniment souvent. On peut aussi faire porter ces conditions sur desensembles de transitions.Depuis 2014, de nombreux outils académiques produisant des ω-automatesse sont accordés sur l'utilisation d'un format d'échange textuel, leformat HOA (Hanoi Omega Automata). Dans ce format, les conditionsd'acceptation sont spécifiées, non pas par leur nom, mais sous laforme d'une formule Booléenne exprimant exactement quels ensemblesd'états (ou de transitions) doivent être vus finiment souvent ouinfiniment souvent. Par exemple une condition de Rabin avec 2 pairespourra être exprimée sous la forme (Fin(0)&Inf(1))|(Fin(2)&Inf(3))signifiant que soit les ensembles (d'états ou transitions) numérotés 0et 1 doivent être vus respectivement finiment et infiniment souvent,soit ensembles 2 et 3 sont vus finiment et infiniment souvent.
Doctorant.e: Renkin Florian