Difference between revisions of "Publications/michaud.15.spin"
From LRDE
| Line 5: | Line 5: | ||
| title = Practical Stutter-Invariance Checks for ω-Regular Languages |
| title = Practical Stutter-Invariance Checks for ω-Regular Languages |
||
| 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 = 84 to 101 |
| + | | volume = 9232 |
||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
| publisher = Springer |
| publisher = Springer |
||
| Line 12: | Line 13: | ||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-06-15 |
| lrdenewsdate = 2015-06-15 |
||
| + | | lrdepaper = http://www.lrde.epita.fr/dload/papers/michaud.15.spin.pdf |
||
| − | | note = To appear |
||
| type = inproceedings |
| type = inproceedings |
||
| id = michaud.15.spin |
| id = michaud.15.spin |
||
| + | | identifier = doi:10.1007/978-3-319-23404-5_7 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> michaud.15.spin, |
@InProceedings<nowiki>{</nowiki> michaud.15.spin, |
||
| Line 23: | Line 25: | ||
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>84--101<nowiki>}</nowiki>, |
| + | volume = 9232, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
| Line 40: | Line 44: | ||
can easily check whether an LTL or PSL formula is |
can easily check whether an LTL or PSL formula is |
||
stutter-invariant.<nowiki>}</nowiki>, |
stutter-invariant.<nowiki>}</nowiki>, |
||
| − | + | doi = <nowiki>{</nowiki>10.1007/978-3-319-23404-5_7<nowiki>}</nowiki> |
|
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 17:42, 31 August 2015
- Authors
- Thibaud Michaud, Alexandre Duret-Lutz
- 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
We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns outimplementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant.
Documents
Bibtex (lrde.bib)
@InProceedings{ michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for {$\omega$}-Regular
Languages},
booktitle = {Proceedings of the 22th International SPIN Symposium on
Model Checking of Software (SPIN'15)},
year = 2015,
month = aug,
pages = {84--101},
volume = 9232,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
abstract = {We propose several automata-based constructions that check
whether a specification is stutter-invariant. These
constructions assume that a specification and its negation
can be translated into B{\"u}chi automata, but aside from
that, they are independent of the specification formalism.
These transformations were inspired by a construction due
to Holzmann and Kupferman, but that we broke down into two
operations that can have different realizations, and that
can be combined in different ways. As it turns out,
implementing only one of these operations is needed to
obtain a functional stutter-invariant check. Finally we
have implemented these techniques in a tool so that users
can easily check whether an LTL or PSL formula is
stutter-invariant.},
doi = {10.1007/978-3-319-23404-5_7}
}