Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1196458,
author = {Blahoudek, František and DuretandLutz, Alexandre and Křetínský, Mojmír and Strejček, Jan},
address = {New York},
booktitle = {2014 International SPIN Symposium on Model Checking of Software},
doi = {http://dx.doi.org/10.1145/2632362.2632377},
editor = {Neha Rungta and Oksana Tkachuk},
keywords = {linear temporal logic; Büchi automata; explicit model checking},
howpublished = {tištěná verze "print"},
language = {eng},
location = {New York},
isbn = {978-1-4503-2452-6},
pages = {68-76},
publisher = {ACM},
title = {Is there a best Büchi automaton for explicit model checking?},
year = {2014}
}
TY - JOUR
ID - 1196458
AU - Blahoudek, František - Duret-Lutz, Alexandre - Křetínský, Mojmír - Strejček, Jan
PY - 2014
TI - Is there a best Büchi automaton for explicit model checking?
PB - ACM
CY - New York
SN - 9781450324526
KW - linear temporal logic
KW - Büchi automata
KW - explicit model checking
N2 - LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
ER -
BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Is there a best Büchi automaton for explicit model checking? In Neha Rungta and Oksana Tkachuk. \textit{2014 International SPIN Symposium on Model Checking of Software}. New York: ACM, 2014, p.~68-76. ISBN~978-1-4503-2452-6. Available from: https://dx.doi.org/10.1145/2632362.2632377.
|
