Nondeterminisation of alternating automata in SPOT



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.