Difference between revisions of "Publications/blahoudek.15.spin"
From LRDE
| Line 5: | Line 5: | ||
| title = On Refinement of Büchi Automata for Explicit Model Checking |
| title = On Refinement of Büchi Automata for Explicit Model Checking |
||
| booktitle = Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15) |
| booktitle = Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15) |
||
| − | | pages = |
+ | | pages = 66 to 83 |
| publisher = Springer |
| publisher = Springer |
||
| + | | volume = 9232 |
||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
| urllrde = 201508-Spin1 |
| urllrde = 201508-Spin1 |
||
| Line 12: | Line 13: | ||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-06-15 |
| lrdenewsdate = 2015-06-15 |
||
| + | | lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.15.spin.pdf |
||
| − | | note = To appear |
||
| type = inproceedings |
| type = inproceedings |
||
| id = blahoudek.15.spin |
| id = blahoudek.15.spin |
||
| + | | identifier = doi:10.1007/978-3-319-23404-5_6 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> blahoudek.15.spin, |
@InProceedings<nowiki>{</nowiki> blahoudek.15.spin, |
||
| Line 24: | Line 26: | ||
Model Checking of Software (SPIN'15)<nowiki>}</nowiki>, |
Model Checking of Software (SPIN'15)<nowiki>}</nowiki>, |
||
year = 2015, |
year = 2015, |
||
| + | month = aug, |
||
| − | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>66--83<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
| + | volume = 9232, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki>In explicit model checking, systems are typically |
abstract = <nowiki>{</nowiki>In explicit model checking, systems are typically |
||
| Line 37: | Line 41: | ||
that are easier to understand and, more importantly, for |
that are easier to understand and, more importantly, for |
||
which the explicit model checking process performs better.<nowiki>}</nowiki>, |
which the explicit model checking process performs better.<nowiki>}</nowiki>, |
||
| − | + | doi = <nowiki>{</nowiki>10.1007/978-3-319-23404-5_6<nowiki>}</nowiki> |
|
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 17:40, 31 August 2015
- Authors
- František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, Jan Strejček
- Where
- Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2015-06-15
Abstract
In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.
Documents
Bibtex (lrde.bib)
@InProceedings{ blahoudek.15.spin,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Vojt\v{c}ech Rujbr and Jan Strej\v{c}ek},
title = {On Refinement of {B\"u}chi Automata for Explicit Model
Checking},
booktitle = {Proceedings of the 22th International SPIN Symposium on
Model Checking of Software (SPIN'15)},
year = 2015,
month = aug,
pages = {66--83},
publisher = {Springer},
volume = 9232,
series = {Lecture Notes in Computer Science},
abstract = {In explicit model checking, systems are typically
described in an implicit and compact way. Some valid
information about the system can be easily derived directly
from this description, for example that some atomic
propositions cannot be valid at the same time. The paper
shows several ways to apply this information to improve the
B{\"u}chi automaton built from an LTL specification. As a
result, we get smaller automata with shorter edge labels
that are easier to understand and, more importantly, for
which the explicit model checking process performs better.},
doi = {10.1007/978-3-319-23404-5_6}
}