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
• TeamMoVe
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.