Bisimulation-based Reductions on TGBA

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 ${\displaystyle {\mathcal {\omega }}}$-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.