Comparison of Algorithms for Checking Emptiness on Büchi Automata

Andreas Gaiser Stefan Schwoon 1
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We re-investigate the problem of LTL model-checking for finite-state systems. Typical solutions, like in Spin, work on the fly, reducing the problem to Buechi emptiness. This can be done in linear time, and a variety of algorithms with this property exist. Nonetheless, subtle design decisions can make a great difference to their actual performance in practice, especially when used on-the-fly. We compare a number of algorithms experimentally on a large benchmark suite, measure their actual run-time performance, and propose improvements. Compared with the algorithm implemented in Spin, our best algorithm is faster by about 33 % on average. We therefore recommend that, for on-the-fly explicit-state model checking, nested DFS should be replaced by better solutions.
Type de document :
Communication dans un congrès
MEMICS, Nov 2009, Znojmo, Czech Republic. 2009
Liste complète des métadonnées
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 19:48:45
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37


  • HAL Id : hal-00772632, version 1



Andreas Gaiser, Stefan Schwoon. Comparison of Algorithms for Checking Emptiness on Büchi Automata. MEMICS, Nov 2009, Znojmo, Czech Republic. 2009. 〈hal-00772632〉



Consultations de la notice