Model Checking using Generalized Testing Automata

From LRDE

Revision as of 10:29, 1 April 2019 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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.

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.

Documents

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},
  doi		= {10.1007/978-3-642-35179-2_5},
  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.}
}