La complémentation d'automates de Büchi à travers des automates alternants

From LRDE

Résumé

Le model checking est un domaine de la vérification formelle, qui permet de vérifier le comportement d'un système avec l'aide de formules logiques temporelles. Spot est une bibliothèque de model checking qui repose sur une des techniques du domaine : l'approche automate. Dans cette approche du model checking, le système et les formules sont représentés sous forme d'automates acceptant des mots de longueur infinie, et plus particulièrement des automates de Büchi. Spot propose de nombreux algorithmes aux utilisateurs de la bibliothèque pour manipuler ce type d'automates, en vue d'applications au model checking. Une opération sur ces automates a récemment été ajoutée dans Spot : la complémentation. La recherche d'algorithmes effectuant cette opération est toujours d'actualité puisqu'il n'existe toujours pas d'algorithme atteignant les bornes théoriques optimales. Nous présenterons deux algorithmes récents de complémentation que nous venons d'ajouter dans Spot, qui se basent sur des automates alternants.