Abstract
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 signi cantly 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.
| Original language | English |
|---|---|
| Title of host publication | SPIN 2017 |
| Subtitle of host publication | Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software |
| Publisher | Association for Computing Machinery (ACM) |
| Pages | 50-59 |
| Number of pages | 10 |
| ISBN (Print) | 978-1-4503-5077-8 |
| DOIs | |
| Publication status | Published - Jul 2017 |
| Event | 24th International SPIN Symposium 2017: Model Checking of Software - University of California, Santa Barbara, United States Duration: 13 Jul 2017 → 14 Jul 2017 Conference number: 24 http://conf.researchr.org/home/spin-2017 |
Conference
| Conference | 24th International SPIN Symposium 2017 |
|---|---|
| Abbreviated title | SPIN 2017 |
| Country | United States |
| City | Santa Barbara |
| Period | 13/07/17 → 14/07/17 |
| Internet address |
Fingerprint
Keywords
- Model checking
- Explicit state
- LTL
- omega-automata
- on-the-fly
- generalised Büchi Automaton
- generalised Rabin Automaton
- parallel algorithms
- multi-core
Cite this
}
Explicit State Model Checking with Generalized Büchi and Rabin Automata. / Bloemen, Vincent; Duret-Lutz, Alexandre; van de Pol, Jaco.
SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. Association for Computing Machinery (ACM), 2017. p. 50-59.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - Explicit State Model Checking with Generalized Büchi and Rabin Automata
AU - Bloemen, Vincent
AU - Duret-Lutz, Alexandre
AU - van de Pol, Jaco
PY - 2017/7
Y1 - 2017/7
N2 - 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 signi cantly 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.
AB - 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 signi cantly 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.
KW - Model checking
KW - Explicit state
KW - LTL
KW - omega-automata
KW - on-the-fly
KW - generalised Büchi Automaton
KW - generalised Rabin Automaton
KW - parallel algorithms
KW - multi-core
U2 - 10.1145/3092282.3092288
DO - 10.1145/3092282.3092288
M3 - Conference contribution
SN - 978-1-4503-5077-8
SP - 50
EP - 59
BT - SPIN 2017
PB - Association for Computing Machinery (ACM)
ER -