• Home
  • Page : 'rapport_recherche' inconnue (menus.php)

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
  • 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.
  • Keywords : model-checking, emptiness check, verification, Büchi automata, inclusion, symmetries, reduction
  • Publisher : Thierry.Lanfroy (at) nulllip6.fr
Mentions légales
Site map