DROPS.MEMICS.2009.2349.pdf
- Filesize: 352 kB
- 9 pages
Document
Comparison of Algorithms for Checking Emptiness on Büchi Automata
Authors
-
Part of:
Volume:
Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (MEMICS 2009)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2009-12-15
Cite AsGet BibTex
Andreas Gaiser and Stefan Schwoon. Comparison of Algorithms for Checking Emptiness on Büchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 18-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
https://doi.org/10.4230/DROPS.MEMICS.2009.2349
https://doi.org/10.4230/DROPS.MEMICS.2009.2349
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.
Keywords
- LTL Model checking
- Depth first search
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads