Direct-Simulation Reduction for TGBA

From LRDE

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 and to consume the memory as less as possible. A good way to reach that is to make automata as small as possible. Scientific litterature proposes a lot of algorithm to achieve this goal. Simulation works on automata which recognizes words of infinite length thanks to acceptance states. We see in this work how to adapt this algorithm to make it works on TGBA. We will see the profit which is given by the simulation implementation on Spot.