Mrudula BALACHANDER - Faculté des Sciences

Titre de la thèse: "Towards practical synthesis based on automata learning and succinct representations"

Résumé:
Les systèmes réactifs sont des systèmes informatiques qui interagissent continuellement avec leur environnement et exigent des normes élevées de fiabilité et d'efficacité. Leur conception est intrinsèquement complexe, et le risque de défaillances dues à des interactions imprévues est constant. Pour renforcer la fiabilité de ces systèmes, les méthodes formelles de vérification se sont avérées particulièrement utiles.

Cette thèse se concentre sur la synthèse réactive, qui vise à automatiser la construction de systèmes réactifs, à partir de spécifications données dans des langages abstraits et haut-niveau tel que des logiques, et notamment la logique temporelle LTL. Ce travail vise à faire progresser le domaine de la synthèse selon deux axes principaux, adressant les limites pratiques des approches existantes.

Axe I : Amélioration de la Synthèse LTL, basée sur l'apprentissage passif
Nous abordons les limites inhérentes aux méthodes de synthèse LTL standards, qui produisent souvent des contrôleurs non intuitifs ou inefficaces. Nous introduisons pour cela la « Synthèse LTL avec exemples » (LTL synthesis with hints), une extension du problème de synthèse avec des exemples. Plus précisément, cette approche intègre des exemples d'exécution fournis par l'utilisateur afin de guider les algorithmes de synthèse. Notre méthode combine efficacement des techniques d'apprentissage passif, afin de généraliser les exemples fournis, avec des algorithmes de synthèse LTL classiques. Cette intégration permet de combler le fossé entre la nécessité d'écrire des spécifications logiques abstraites, mais aussi celle d'avoir des implémentations pratiques et efficaces, comme le démontrent notre prototype et nos études de cas.

Axe II : Représentations Efficaces des Contrôleurs
Les systèmes réactifs générés par les algorithmes traditionnels de synthèse LTL sont représentés par des machines à états finis appelées machines de Mealy. Cependant, elles ont en général un grand nombre d'états, ce qui nuit à l'efficacité des algorithmes ainsi qu'à lisibilité des machines produites. Pour obtenir des représentations de contrôleurs à la fois concises et
performantes, nous explorons la classe des automates à registres (Register Automata), capables de reconnaître des langages réguliers sur des alphabets infinis.
Notre travail introduit une nouvelle variante, les Automates à Registres Déterministes avec Permutations (pDRA). Les pDRA offrent un bon équilibre entre la concision et la complexité des problèmes algorithmiques liés aux automates, notamment le problème d'équivalence.

Nous fournissons également une caractérisation de type Myhill-Nerode pour cette nouvelle classe d'automates, ce qui permet la construction de représentations minimales et canoniques. De plus, nous présentons un algorithme d'apprentissage passif de complexité polynomiale pour une sous-classe de ces automates, démontrant leur identification efficace à la limite.

Ces contributions représentent une étape importante vers des méthodes de synthèse de systèmes réactifs plus robustes, plus efficaces et permettant des applications concrètes de la synthèse en pratique.