Comparison of Algorithms for Checking Emptiness on Büchi Automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Comparison of Algorithms for Checking Emptiness on Büchi Automata

Résumé

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.

Domaines

Autre [cs.OH]
Fichier non déposé

Dates et versions

hal-00772632 , version 1 (10-01-2013)

Identifiants

  • HAL Id : hal-00772632 , version 1

Citer

Andreas Gaiser, Stefan Schwoon. Comparison of Algorithms for Checking Emptiness on Büchi Automata. MEMICS, Nov 2009, Znojmo, Czech Republic. ⟨hal-00772632⟩
115 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More