Comparison of Algorithms for Checking Emptiness on Büchi Automata

Gaiser, Andreas; Schwoon, Stefan

doi:10.4230/DROPS.MEMICS.2009.2349

Document

Comparison of Algorithms for Checking Emptiness on Büchi Automata

Authors Andreas Gaiser, Stefan Schwoon

Part of: Volume: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (MEMICS 2009)
Part of: Series: Open Access Series in Informatics (OASIcs)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2009-12-15

PDF

File

PDF

DROPS.MEMICS.2009.2349.pdf

Filesize: 352 kB
9 pages

Document Identifiers

DOI: 10.4230/DROPS.MEMICS.2009.2349
URN: urn:nbn:de:0030-drops-23494

Subject Classification

Keywords

LTL Model checking
Depth first search

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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

Author Details

Andreas Gaiser

Stefan Schwoon

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail