Comparison of Algorithms for Checking Emptiness on Büchi Automata

Authors Andreas Gaiser, Stefan Schwoon

Thumbnail PDF


  • Filesize: 352 kB
  • 9 pages

Document Identifiers

Author Details

Andreas Gaiser
Stefan Schwoon

Cite AsGet BibTex

Andreas Gaiser and Stefan Schwoon. Comparison of Algorithms for Checking Emptiness on Büchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 18-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


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 Büchi 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.
  • LTL Model checking
  • Depth first search


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads