Liens transverses ENS de Lyon

Agenda de l'ENS de Lyon

Non-determinism, explorable automata and cyclic proofs

Date
ven 30 sep 2022
Horaires

15H00

Lieu(x)

ENS de Lyon

Intervenant(s)

Soutenance de thèse de M. HAZARD Emile sous la Direction de M. POUS Damien

Langue(s) des interventions

Description générale

Cette thèse est divisée en deux parties, qui ont en commun le problème du non-déterminisme chez différents modèles d'automates, et la résolution de celui-ci.

La première partie s'intéresse à une forme de limitation du non-déterminisme, que l'on nomme l'explorabilité. Un automate est explorable s'il est possible de résoudre le non-déterminisme en créant un nombre finis d'exécutions en parallèle. Il s'agit d'une généralisation de la notion d'automate Good-For-Games, i.e. Bon-Pour-les-Jeux (GFG), qui correspond au cas où une seule exécution suffit. Nous commençons par fournir un lien supplémentaire entre ces deux notions : le fait que l'on peut décider en temps polynomial si un automate est GFG, à condition de savoir qu'il est explorable. Nous montrons ensuite que la reconnaissance des automates GFG est un problème PSPACEcomplet dans le cas des automates de mots finis ou de Büchi. Nous nous intéressons aussi au problème de l'omega-explorabilité, qui correspond au cas où l'on s'autorise un nombre dénombrable d'exécutions. Celui-ci est non-trivial dans le cas des mots infinis, et nous montrons que décider l'omega-explorabilité d'un automate de co-Büchi est EXPTIME-complet.

Dans la seconde partie, nous présentons un système de preuves cycliques permettant de fournir des certificats d'inclusions entre langages de mots infinis. Ces langages sont représentés par des expressions omega-régulières dans un premier temps, puis par une généralisation de ces expressions, qui permet notamment des imbrications de l'opérateur omega. Nous montrons la correction et la complétude de ce système, et fournissons deux résultats algorithmiques : la décidabilité de la validité d'une preuve cyclique, ainsi qu'un algorithme PSPACE pour décider l'inclusion de deux langage par la recherche de preuve.

Gratuit
Mots clés
Disciplines