Difference between revisions of "Publications/bensalem.12.topnoc"
From LRDE
| Line 11: | Line 11: | ||
| urllrde = 2012-TOPNOC |
| urllrde = 2012-TOPNOC |
||
| abstract = Geldenhuys and Hansen showed that a kind of ω-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. |
| abstract = Geldenhuys and Hansen showed that a kind of ω-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 |
| lrdeprojects = Spot |
||
| type = article |
| type = article |
||
Revision as of 01:00, 10 March 2015
- 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 ω-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.
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.}
}