Nondeterminisation of alternating automata in SPOT

Authors

Samuel Da Mota

Type

techreport

Year

2009

Number

0908

Projects

Spot

Keywords

SPOT, model checking, alternating automatanondeterminization, Transition-based Generalized Buchi-Automata

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 formulæ 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 formulæ to alternating automata will be added.