Generalized Büchi Automata versus Testing Automata for Model Checking

From LRDE

Abstract

Geldenhuys and Hansen have shown that a kind of Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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

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