Comparison of Algorithms for Checking Emptiness on Buechi Automata

Andreas Gaiser, Stefan Schwoon

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 b…