Model Checking using Generalized Testing Automata

Authors

Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon

Journal

Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI)

Type

article

Publisher

Springer-Verlag

Projects

Spot

Date

2012-01-01

Abstract

Geldenhuys and Hansen showed that a kind of ω-automa­ta known as Testing Automata (TA) can, in the case of stuttering-insensitive propertiesoutperform the Buchi automata traditionally used in the automata-theoretic approach to model checking. In previous work, we compared TA against Transition-based Generalized Buchi Automata (TGBA)and concluded that TA were more interesting when counterexamples were expected, otherwise TGBA were more efficient. In this work we introduce a new kind of automata, dubbed emphTransition-based Generalized Testing Automata (TGTA), that combine ideas from TA and TGBA. Implementation and experimentation of TGTA show that they outperform other approaches in most of the cases.

Bibtex (lrde.bib)

@Article{	  bensalem.12.topnoc,
  author	= {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
		  Fabrice Kordon},
  title		= {Model Checking using Generalized Testing Automata},
  journal	= {Transactions on Petri Nets and Other Models of Concurrency
		  (ToPNoC VI)},
  year		= 2012,
  volume	= 7400,
  series	= {Lecture Notes in Computer Science},
  isbn		= {978-3-642-35178-5},
  publisher	= {Springer-Verlag},
  pages		= {94--112},
  abstract	= {Geldenhuys and Hansen showed that a kind of
		  $\omega$-automa\-ta known as \emph{Testing Automata} (TA)
		  can, in the case of stuttering-insensitive properties,
		  outperform the Buchi automata traditionally used in the
		  automata-theoretic approach to model
		  checking~\cite{geldenhuys.06.spin}. In previous
		  work~\cite{bensalem.sumo.2011}, we compared TA against
		  \emph{Transition-based Generalized Buchi Automata} (TGBA),
		  and concluded that TA were more interesting when
		  counterexamples were expected, otherwise TGBA were more
		  efficient. In this work we introduce a new kind of
		  automata, dubbed \emph{Transition-based Generalized Testing
		  Automata} (TGTA), that combine ideas from TA and TGBA.
		  Implementation and experimentation of TGTA show that they
		  outperform other approaches in most of the cases.}
}