Bisimulation-based Reductions on TGBA

From LRDE

Revision as of 17:03, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Thomas Badie | title = Bisimulation-based Reductions on TGBA | year = 2011 | abstract = Spot is a C++ library that relies on the automata theoretic app...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

Spot is a C++ library that relies on the automata theoretic approach to model checking. To represent properties we use LTL-formulae, which are translated into automata. In Spot these automata are Transition-based Generalized Büchi Automata (TGBA). A major issue for a model checker is to be fast. A good way to reach that is to make automata as small as possible. Scientific litterature proposes a lot of algorithm to achieve our goal. Bisimulation and simulation work on -automata. We see in this report how to adapt these algorithms to make them work on TGBA. We will see the profit which is given by the bisimulation implementation. And we deduce the importance to implement the simulation to reduce TGBA.