LIP6 2006/003

• 技术报告 «Test de vacuité d'automates de Büchi ensemblistes en utilisant des tests d'inclusion.»
• S. Baarir, A. Duret-Lutz
• 18 pages - 2006-10-11 - document en - http://www.lip6.fr/lip6/reports/2006/lip6-2006-003.pdf 278 Ko
• 联系方式 Alexandre.Duret-Lutz (at) nulllip6.fr
• 科研组MoVe
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.