Gaiser, Andreas ;
Schwoon, Stefan
Comparison of Algorithms for Checking Emptiness on Büchi Automata
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.
BibTeX - Entry
@InProceedings{gaiser_et_al:OASIcs:2009:2349,
author = {Andreas Gaiser and Stefan Schwoon},
title = {{Comparison of Algorithms for Checking Emptiness on B{\"u}chi Automata}},
booktitle = {Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
pages = {18--26},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-939897-15-6},
ISSN = {2190-6807},
year = {2009},
volume = {13},
editor = {Petr Hlinen{\'y} and V{\'a}clav Maty{\'a}{\v{s}} and Tom{\'a}{\v{s}} Vojnar},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2009/2349},
URN = {urn:nbn:de:0030-drops-23494},
doi = {http://dx.doi.org/10.4230/DROPS.MEMICS.2009.2349},
annote = {Keywords: LTL Model checking, Depth first search}
}
|
Keywords: |
|
LTL Model checking, Depth first search |
|
Seminar: |
|
Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)
|
|
Issue date: |
|
2009 |
|
Date of publication: |
|
2009 |
