Selected publications by Stefan Schwoon

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

@inproceedings{GS-memics09,
   address = {Znojmo, Czech Republic},
   author = {Gaiser, Andreas and Schwoon, Stefan},
   booktitle = {{P}roceedings of the 5th {A}nnual {D}octoral {W}orkshop on {M}athematical and {E}ngineering {M}ethods in {C}omputer {S}cience ({MEMICS}'09)},
   editor = {Hlin{\v e}n{\'y}, Petr and Maty{\'a}{\v s}, V{\'a}clav and Vojnar, Tom{\'a}{\v{s}}},
   month = nov,
   title = {Comparison of algorithms for checking emptiness on B{\"u}chi automata},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GS-memics09.pdf},
   year = {2009},
}

About LSV