Generalized Büchi Automata versus Testing Automata for Model Checking
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon
- Where
- Proceedings of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO'11)
- Place
- Newcastle, UK
- Type
- inproceedings
- Publisher
- CEUR
- Projects
- Spot
- Date
- 2011-05-25
Abstract
Geldenhuys and Hansen have shown that a kind of -automaton known as testing automata can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking. This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).
Documents
Bibtex (lrde.bib)
@InProceedings{ bensalem.11.sumo, author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and Fabrice Kordon}, title = {Generalized {B\"u}chi Automata versus Testing Automata for Model Checking}, booktitle = {Proceedings of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO'11)}, address = {Newcastle, UK}, series = {Workshop Proceedings}, year = 2011, month = jun, volume = 726, publisher = {CEUR}, url = {http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-726/}, abstract = {Geldenhuys and Hansen have shown that a kind of $\omega$-automa\-ton known as \emph{testing automata} can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking~\cite{geldenhuys.06.spin}. This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formul\ae{} (for which testing automata fare better) from verified formul\ae{} (where testing automata are hindered by their two-pass emptiness check).} }