View source for Publications/bensalem.12.topnoc

{{Publication
| published = true
| date = 2012-01-01
| authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon
| title = Model Checking using Generalized Testing Automata
| journal = Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI)
| volume = 7400
| series = Lecture Notes in Computer Science
| publisher = Springer-Verlag
| pages = 94 to 112
| abstract = Geldenhuys and Hansen showed that a kind of <math>\omega</math>-automata 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.
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.12.topnoc.pdf
| lrdeprojects = Spot
| type = article
| id = bensalem.12.topnoc
| identifier = doi:10.1007/978-3-642-35179-2_5
| bibtex = 
@Article<nowiki>{</nowiki>	  bensalem.12.topnoc,
  author	= <nowiki>{</nowiki>Ala Eddine Ben<nowiki>{</nowiki> S<nowiki>}</nowiki>alem and Alexandre Duret-Lutz and
		  Fabrice Kordon<nowiki>}</nowiki>,
  title		= <nowiki>{</nowiki>Model Checking using Generalized Testing Automata<nowiki>}</nowiki>,
  journal	= <nowiki>{</nowiki>Transactions on Petri Nets and Other Models of Concurrency
		  (ToPNoC VI)<nowiki>}</nowiki>,
  year		= 2012,
  volume	= 7400,
  series	= <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  isbn		= <nowiki>{</nowiki>978-3-642-35178-5<nowiki>}</nowiki>,
  publisher	= <nowiki>{</nowiki>Springer-Verlag<nowiki>}</nowiki>,
  doi		= <nowiki>{</nowiki>10.1007/978-3-642-35179-2_5<nowiki>}</nowiki>,
  pages		= <nowiki>{</nowiki>94--112<nowiki>}</nowiki>,
  abstract	= <nowiki>{</nowiki>Geldenhuys and Hansen showed that a kind of
		  $\omega$-automa\-ta known as \emph<nowiki>{</nowiki>Testing Automata<nowiki>}</nowiki> (TA)
		  can, in the case of stuttering-insensitive properties,
		  outperform the Buchi automata traditionally used in the
		  automata-theoretic approach to model
		  checking~\cite<nowiki>{</nowiki>geldenhuys.06.spin<nowiki>}</nowiki>. In previous
		  work~\cite<nowiki>{</nowiki>bensalem.sumo.2011<nowiki>}</nowiki>, we compared TA against
		  \emph<nowiki>{</nowiki>Transition-based Generalized Buchi Automata<nowiki>}</nowiki> (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<nowiki>{</nowiki>Transition-based Generalized Testing
		  Automata<nowiki>}</nowiki> (TGTA), that combine ideas from TA and TGBA.
		  Implementation and experimentation of TGTA show that they
		  outperform other approaches in most of the cases.<nowiki>}</nowiki>
<nowiki>}</nowiki>

}}