Simulation-based Reductions for TGBA
From LRDE
- Authors
- Thomas Badie
- Type
- techreport
- Year
- 2013
- Number
- 1214
- Projects
- Spot
- Keywords
- automata, BDD, bisimulation, simulation, model checkingreduction, TGBA
Abstract
The Automata-Theoretic approach to model checking traditionally relies on Büchi Automata (BA) which we want as small as possible. Spot, a model-checking library, uses mainly TGBA: a BA generalization. We have already presented a simulation reduction (called direct) that works on TGBA. This algorithm is included in Spot 0.9 and led to produce smaller automata than in the previous versions of Spot. The simulation consists in merging states that recognize the same infinite suffixes. We show that we can also work on infinite prefixes (it is called cosimulation), and that we can iterate these two simulations to create the iterated simulation. This iteration-based simulation, included in Spot 1.0, is a clear improvement over our previous simulation procedure. We finally experiment a method that consists in considering some acceptance conditions as don't care. Since the acceptance conditions on transitions that are not on a Strongly Connected Component have no influence on the language, we can change them to help the simulations.