LIP6 2006/003
- Technical report
Test de vacuité d'automates de Büchi ensemblistes en utilisant des tests d'inclusion. - S. Baarir, A. Duret-Lutz
- 18 pages - 10/11/2006- document en - http://www.lip6.fr/lip6/reports/2006/lip6-2006-003.pdf - 278 Ko
- Contact : Alexandre.Duret-Lutz (at) nulllip6.fr
- Team : MoVe
- Keywords : model-checking, emptiness check, verification, Büchi automata, inclusion, symmetries, reduction
- Publisher : Thierry.Lanfroy (at) nulllip6.fr
A possible attack on the state explosion of the automata-theoretic approach to model-checking is to build an automaton B whose states represent sets of states of the original automaton A to check for emptiness.
This paper introduces two emptiness checks for Büchi automata whose states represent sets that may include each other. The first check on B is equivalent to a traditional emptiness check on A but uses inclusion tests to direct and further reduce the on-the-fly construction of B. The second check is impressively faster but may return false negatives. We illustrate and benchmark both using a symmetry-based reduction.
This paper introduces two emptiness checks for Büchi automata whose states represent sets that may include each other. The first check on B is equivalent to a traditional emptiness check on A but uses inclusion tests to direct and further reduce the on-the-fly construction of B. The second check is impressively faster but may return false negatives. We illustrate and benchmark both using a symmetry-based reduction.