Non-determinism, explorable automata and cyclic proofs
Non-déterminisme, automates explorables et preuves cycliques
Résumé
This thesis is divided into two main parts, although a common denominator can be found in the notion of non-determinism in automata, and its resolution. The first part focuses on a notion of limited non-determinism, which is explorable automata. These are automata for which the non-determinism can be resolved by building a finite number of simultaneous runs. This generalizes the notion of Good-For-Games (GFG) automata, which correspond to the case where a single run is enough. We give another link between these two notions, namely the fact that GFGness is decidable in PTIME for explorable automata. We prove that deciding whether an automaton is explorable is an EXPTIME-complete problem for finite and Büchi automata. We also consider the problem of omega-explorability, in which we allow for a countable number of simultaneous runs. This problem is non-trivial for automata of infinite words, and we prove the EXPTIME-completeness of deciding the omega-explorability of a co-Büchi automaton. In the second part, we describe a cyclic proof system designed to provide certificates of inclusions between languages of infinite words. These languages are represented by omega-regular expressions, or in the final version by a generalization of these expressions, allowing for arbitrary nesting of the omega operator. We prove the soundness and completeness of that system, along with some algorithmic results: the decidability of the validity of a cyclic proof, and a PSPACE proof search algorithm to decide the inclusion of languages.
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 PSPACE-complet 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 langages par la recherche de preuve.
Origine : Version validée par le jury (STAR)