Samuel Da Mota. Nondeterminisation of alternating automata in SPOT. CSI Seminar 0908 June 2009

Abstract

SPOT is a C++ model checking library that relies on the automata theoretic approach to model checking. The first step of this approach consists in the translation of an LTL formula to an automaton that recognizes the same language. Currently, there exists two algorithms in SPOT that translate LTL formulae to transition based generalized Büchi automata (TGBA). We want to implement a third translation for comparison. This new method translates the LTL formula into an alternating automaton, and then applies a nondeterminisation algorithm which takes as input the alternating automaton and gives out a TGBA.

To complete this task, the alternating automaton structure will first be set up in SPOT, then the nondeterminization algorithm will be implemented, and last, the translation of LTL formulae to alternating automata will be added.

Résumé

SPOT est une bibliothèque de \emph{model checking} basée sur l'approche par automates et sur les automates de Büchi généralisé basé sur les transitions (TGBA) pour la vérification de systèmes exprimés sous forme de formules logiques. L'approche automate consite à traduire une formule logique LTL en un automate qui reconnait 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 altenants 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.
to top