Explicit State Model Checking with Generalized Büchi and Rabin Automata

Vincent Bloemen; Alexandre Duret-Lutz; Jaco van de Pol

doi:10.1145/3092282.3092288

Explicit State Model Checking with Generalized Büchi and Rabin Automata

Vincent Bloemen, Alexandre Duret-Lutz, Jaco van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

3 Downloads (Pure)

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 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	https://doi.org/10.1145/3092282.3092288
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	http://conf.researchr.org/home/spin-2017

Keywords

Model checking
Explicit state
LTL
omega-automata
on-the-fly
generalised Büchi Automaton
generalised Rabin Automaton
parallel algorithms
multi-core

Access to Document

10.1145/3092282.3092288

Fingerprint Dive into the research topics of 'Explicit State Model Checking with Generalized Büchi and Rabin Automata'. Together they form a unique fingerprint.

Cite this

@inproceedings{b62cb58beb1249398e18ad39009fab27,

title = "Explicit State Model Checking with Generalized B{\"u}chi and Rabin Automata",

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{\"u}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.",

keywords = "Model checking, Explicit state, LTL, omega-automata, on-the-fly, generalised B{\"u}chi Automaton, generalised Rabin Automaton, parallel algorithms, multi-core ",

author = "Vincent Bloemen and Alexandre Duret-Lutz and {van de Pol}, Jaco",

year = "2017",

month = jul,

doi = "10.1145/3092282.3092288",

language = "English",

isbn = "978-1-4503-5077-8",

pages = "50--59",

booktitle = "SPIN 2017",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "24th International SPIN Symposium 2017 : Model Checking of Software, SPIN 2017 ; Conference date: 13-07-2017 Through 14-07-2017",

url = "http://conf.researchr.org/home/spin-2017",

}

Bloemen, V, Duret-Lutz, A & van de Pol, J 2017, Explicit State Model Checking with Generalized Büchi and Rabin Automata. in SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. Association for Computing Machinery (ACM), pp. 50-59, 24th International SPIN Symposium 2017, Santa Barbara, United States, 13/07/17. https://doi.org/10.1145/3092282.3092288

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

N1 - Conference code: 24

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)

T2 - 24th International SPIN Symposium 2017

Y2 - 13 July 2017 through 14 July 2017

ER -