Difference between revisions of "Publications/bloemen.17.spin"
From LRDE
Line 13: | Line 13: | ||
| type = inproceedings |
| type = inproceedings |
||
| id = bloemen.17.spin |
| id = bloemen.17.spin |
||
+ | | identifier = doi:10.1145/3092282.3092288 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> bloemen.17.spin, |
@InProceedings<nowiki>{</nowiki> bloemen.17.spin, |
||
Line 25: | Line 26: | ||
publisher = <nowiki>{</nowiki>ACM<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>ACM<nowiki>}</nowiki>, |
||
month = jul, |
month = jul, |
||
+ | doi = <nowiki>{</nowiki>10.1145/3092282.3092288<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki>In the automata theoretic approach to explicit state LTL |
abstract = <nowiki>{</nowiki>In the automata theoretic approach to explicit state LTL |
||
model checking, the synchronized product of the model and |
model checking, the synchronized product of the model and |
Latest revision as of 11:29, 1 April 2019
- Authors
- Vincent Bloemen, Alexandre Duret-Lutz, Jaco van de Pol
- Where
- Proceedings of the 24th International SPIN Symposium on Model Checking of Software (SPIN'17)
- Type
- inproceedings
- Publisher
- ACM
- Projects
- Spot
- Date
- 2017-05-22
Abstract
In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure. This paper investigates whether using a more general form of acceptance, namely transition-based generalized Rabin automata (TGRAs), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAshowever the corresponding emptiness checking procedure is more involved. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice. We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest. We observed that our algorithm can be used to replace a TGBA checking algorithm without losing performance. In general, we found little to no improvement by checking TGRAs directly.
Documents
Bibtex (lrde.bib)
@InProceedings{ bloemen.17.spin, author = {Vincent Bloemen and Alexandre Duret-Lutz and Jaco van de Pol}, title = {Explicit State Model Checking with Generalized B{\"u}chi and Rabin Automata}, booktitle = {Proceedings of the 24th International SPIN Symposium on Model Checking of Software (SPIN'17)}, pages = {50--59}, year = {2017}, publisher = {ACM}, month = jul, doi = {10.1145/3092282.3092288}, abstract = {In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) B\"uchi automaton (TGBA) is used for this procedure. This paper investigates whether using a more general form of acceptance, namely transition-based generalized Rabin automata (TGRAs), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice. We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest. We observed that our algorithm can be used to replace a TGBA checking algorithm without losing performance. In general, we found little to no improvement by checking TGRAs directly.} }