Jobs/PHD 2019 omegalgo

From LRDE

Revision as of 11:15, 28 March 2019 by Alexandre Duret-Lutz (talk | contribs) (Created page with "{{Job |Reference id=PHD 2019 omegalgo |Title=Algorithmique des ω-automates |Dates=2019 |Research field=Automates et vérification |Related project=Spot |Advisor=Alexandre Dur...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
Algorithmique des ω-automates
Reference id

PHD 2019 omegalgo

Dates

2019

Research field

Automates et vérification

Related project

Spot

Advisor

Alexandre Duret-Lutz, Adrien Pommellet

General presentation of the field

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 sont

acceptants ou rejetants. Des conditions d'acceptation classiques sont connues sous le nom de conditions de Büchi, de Rabin, de Streett, de Muller, de parité, etc. Elle correspondent à des contraintes sur des ensembles d'états qui doivent être visités infiniment souvent, ou finiment souvent. On peut aussi faire porter ces conditions sur des ensembles de transitions.

Depuis 2014, de nombreux outils académiques produisant des ω-automates se sont accordés sur l'utilisation d'un format d'échange textuel, le format HOA (Hanoi Omega Automata). Dans ce format, les conditions d'acceptation sont spécifiées, non pas par leur nom, mais sous la forme d'une formule Booléenne exprimant exactement quels ensembles d'états (ou de transitions) doivent être vus finiment souvent ou infiniment souvent. Par exemple une condition de Rabin avec 2 paires pourra ê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 0 et 1 doivent être vus respectivement finiment et infiniment souvent, soit ensembles 2 et 3 sont vus finiment et infiniment souvent. Ce type de formule d'acceptation permet de représenter toutes les conditions nommées précédemment, ainsi que toutes leurs combinaisons booléennes. Ces dernières n'ont pas forcément de nom, et peuvent ne pas avoir été étudiées.

Une telle expressivité avait déjà été étudiée par Emerson et Lei (1987), avec une classe d'automates nommée ensuite par d'autres auteurs les "EL-automata". On leur doit quelques résultats comme le fait que le test du vide d'un automate "EL" est NP-complet. L'absence d'applications concrètes, d'outillage, et la dominance des conditions d'acceptation plus simples (Büchi, Streett, Rabin, parité) a probablement contribué a faire tomber les automates EL dans l'oubli.

Aujourd'hui, le contexte est différent. Le format HOA permet de représenter les automates EL (en les généralisant un peu, car il autorise les conditions d'acceptation à porter sur les transitions au lieu des états, ainsi que les automates alternants). De nouvelles conditions d'acceptations sont apparues. Par exemple l'utilisation d'une version généralisées de la condition d'acceptation de Rabin permet de gagner des ordres de grandeur en model checking probabiliste. Plusieurs outils existent pour traduire des formules de logique en ω-automates dont la condition d'acceptation est choisie pour tenter de réduire le nombre d'états. Il devient donc utile d'avoir des logiciels capables de manipuler des ω-automates avec toutes formes de conditions d'acceptation : c'est ce que cherche à faire le projet Spot.

Prerequisites

C++

Objectives

Dans Spot, on souhaite être capable d'effectuer des transformations de conditions d'acceptation, on souhaite généraliser les algorithmes qui ont été inventés pour des conditions d'acceptations particulières de façon à traiter des conditions d'acceptation plus larges. C'est le but de ce projet de recherche. Parmi les algorithmes dont la généralisation nous intéresse le plus, citons : les transformations entre divers types de conditions d'acceptation, les simplifications d'ω-automates avec condition d'acceptation quelconque, la déterminisation d'ω-automates avec condition d'acceptation la plus générique possible, le test du vide d'ω-automates construits à la volée, etc.

Benefit for the candidate
References
Place LRDE: How to get to us
Compensation

environ 1750 euros nets/mois pendant 36 mois

Future work opportunities
Contact

adl@lrde.epita.fr