Difference between revisions of "Publications/blahoudek.14.spin"
From LRDE
| Line 5: | Line 5: | ||
| title = Is There a Best Büchi Automaton for Explicit Model Checking? |
| title = Is There a Best Büchi Automaton for Explicit Model Checking? |
||
| booktitle = Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14) |
| booktitle = Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14) |
||
| + | | pages = 68 to 76 |
||
| publisher = ACM |
| publisher = ACM |
||
| urllrde = 201407-Spin |
| urllrde = 201407-Spin |
||
| Line 11: | Line 12: | ||
| lrdenewsdate = 2014-06-16 |
| lrdenewsdate = 2014-06-16 |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.14.spin.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.14.spin.pdf |
||
| − | | note = To appear |
||
| type = inproceedings |
| type = inproceedings |
||
| id = blahoudek.14.spin |
| id = blahoudek.14.spin |
||
| Line 23: | Line 23: | ||
Model Checking of Software (SPIN'14)<nowiki>}</nowiki>, |
Model Checking of Software (SPIN'14)<nowiki>}</nowiki>, |
||
year = 2014, |
year = 2014, |
||
| ⚫ | |||
publisher = <nowiki>{</nowiki>ACM<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>ACM<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki> LTL to B\"uchi automata (BA) translators are |
abstract = <nowiki>{</nowiki> LTL to B\"uchi automata (BA) translators are |
||
| Line 33: | Line 34: | ||
translators and realistic verification tasks. As a result |
translators and realistic verification tasks. As a result |
||
of these experiences, we gain a better insight into the |
of these experiences, we gain a better insight into the |
||
| − | characteristics of automata that work well with Spin. <nowiki>}</nowiki> |
+ | characteristics of automata that work well with Spin. <nowiki>}</nowiki> |
| ⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 17:33, 26 April 2015
- Authors
- František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček
- Where
- Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14)
- Type
- inproceedings
- Publisher
- ACM
- Projects
- Spot
- Date
- 2014-06-16
Abstract
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.
Documents
Bibtex (lrde.bib)
@InProceedings{ blahoudek.14.spin,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Mojm\'{i}r K\v{r}et\'{i}nsk\'{y} and Jan Strej\v{c}ek},
title = {Is There a Best {B\"u}chi Automaton for Explicit Model
Checking?},
booktitle = {Proceedings of the 21th International SPIN Symposium on
Model Checking of Software (SPIN'14)},
year = 2014,
pages = {68--76},
publisher = {ACM},
abstract = { LTL to B\"uchi 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\"uchi
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. }
}