# Model Checking using Generalized Testing Automata

## Abstract

Geldenhuys and Hansen showed that a kind of ${\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.

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