Reference:

Andreas Gaiser and Stefan Schwoon. Comparison of algorithms for checking emptiness on Büchi automata. In Tomáš Vojnar, Petr Hliněný, Vashek Matyáš, and David Antoš, editors, Proceedings of the 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS), pages 69–77, Znojmo, Czechia, November 2009.

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 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 per cent on average. We therefore recommend that, for on-the-fly explicit-state model checking, nested DFS should be replaced by better solutions.

Suggested BibTeX entry:

@inproceedings{GS09a,
    address = {Znojmo, Czechia},
    author = {Andreas Gaiser and Stefan Schwoon},
    booktitle = {Proceedings of the 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS)},
    editor = {Tom\'a\v{s} Vojnar and Petr Hlin\v{e}n\'y and Vashek Maty\'a\v{s} and David Anto\v{s}},
    month = {November},
    pages = {69--77},
    title = {Comparison of Algorithms for Checking Emptiness on {B\"uchi} Automata},
    year = {2009}
}