Comparison of Algorithms for Checking Emptiness on Buechi Automata

TL;DR

This paper compares various algorithms for checking emptiness in Buechi automata used in LTL model-checking, demonstrating that improved algorithms outperform the traditional nested DFS approach in practical runtime performance.

Contribution

The paper provides an experimental comparison of algorithms for Buechi automata emptiness, proposing improvements and showing that alternative algorithms outperform Spin's nested DFS.

Findings

Best algorithm is 33% faster than Spin's implementation.

Subtle design choices significantly impact practical performance.

Recommended replacing nested DFS with more efficient solutions.

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.