Generalized Büchi Automata versus Testing Automata for Model Checking

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 $\omega$-automa­ton 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

• Paper

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).}
}