Nondeterminisation of alternating automata in SPOT

From LRDE

Revision as of 17:04, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Samuel Da Mota | title = Nondeterminisation of alternating automata in SPOT | year = 2009 | abstract = SPOT is a C++ model checking library that relies...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.