Model Checking using Generalized Testing Automata

From LRDE

Revision as of 11:29, 1 April 2019 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

Geldenhuys and Hansen showed 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­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.}
}