Nondéterminisation d'automates alternants dans SPOT

From LRDE

Résumé

SPOT est une bibliothèque de model checking basée sur l'approche par automates et sur les automates de Büchi généralisés basés sur les transitions (TGBA) pour la vérification de systèmes exprimés sous forme de formules logiques. L'approche automate consiste à traduire une formule logique LTL en un automate qui reconnaît le même language. Dans l'état actuel des choses, il existe deux algorithmes dans SPOT de traduction de formules LTL vers des TGBA. Un troisième algorithme y sera rajouté. Ce dernier convertira dans un premier temps la formule LTL en un automate alternant, puis appliquera un algorithme de nondéterminisation sur celui-ci pour obtenir un TGBA. Le but de cette nouvelle implémentation est de mener une comparaison avec les deux autres déjà en place. Pour mener à bien cette tâche, la structure des automates alternants sera intégrée dans SPOT, puis ce sera au tour de l'algorithme de nondéterminisation d'automates alternants vers des TGBA et enfin la traduction de formules LTL sous forme d'automates alternants.