Difference between revisions of "Publications/bensalem.11.sumo"
From LRDE
(Created page with "{{Publication | date = 2011-05-25 | authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon | title = Generalized Büchi Automata versus Testing Automata for Mode...") |
|||
| (142 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| + | | published = true |
||
| date = 2011-05-25 |
| date = 2011-05-25 |
||
| authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon |
| authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon |
||
| Line 8: | Line 9: | ||
| volume = 726 |
| volume = 726 |
||
| publisher = CEUR |
| publisher = CEUR |
||
| − | | urllrde = 201106-SUMO |
||
| None = http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-726/ |
| None = http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-726/ |
||
| − | | abstract = Geldenhuys and Hansen have shown that a kind of |
+ | | abstract = Geldenhuys and Hansen have shown that a kind of <math>\omega</math>-automaton known as testing automata can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking. This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check). |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.11.sumo.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.11.sumo.pdf |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| Line 31: | Line 31: | ||
volume = 726, |
volume = 726, |
||
publisher = <nowiki>{</nowiki>CEUR<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>CEUR<nowiki>}</nowiki>, |
||
| − | url = <nowiki>{</nowiki>http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-726/<nowiki>}</nowiki> |
+ | url = <nowiki>{</nowiki>http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-726/<nowiki>}</nowiki>, |
| − | , |
||
abstract = <nowiki>{</nowiki>Geldenhuys and Hansen have shown that a kind of |
abstract = <nowiki>{</nowiki>Geldenhuys and Hansen have shown that a kind of |
||
$\omega$-automa\-ton known as \emph<nowiki>{</nowiki>testing automata<nowiki>}</nowiki> can |
$\omega$-automa\-ton known as \emph<nowiki>{</nowiki>testing automata<nowiki>}</nowiki> can |
||
Latest revision as of 19:19, 5 January 2018
- Authors
- Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon
- Where
- Proceedings of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO'11)
- Place
- Newcastle, UK
- Type
- inproceedings
- Publisher
- CEUR
- Projects
- Spot
- Date
- 2011-05-25
Abstract
Geldenhuys and Hansen have shown that a kind of -automaton known as testing automata can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking. This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).
Documents
Bibtex (lrde.bib)
@InProceedings{ bensalem.11.sumo,
author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
Fabrice Kordon},
title = {Generalized {B\"u}chi Automata versus Testing Automata for
Model Checking},
booktitle = {Proceedings of the second International Workshop on
Scalable and Usable Model Checking for Petri Net and other
models of Concurrency (SUMO'11)},
address = {Newcastle, UK},
series = {Workshop Proceedings},
year = 2011,
month = jun,
volume = 726,
publisher = {CEUR},
url = {http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-726/},
abstract = {Geldenhuys and Hansen have shown that a kind of
$\omega$-automa\-ton known as \emph{testing automata} can
outperform the Buchi automata traditionally used in the
automata-theoretic approach to model
checking~\cite{geldenhuys.06.spin}. This work completes
their experiments by including a comparison with
generalized Buchi automata; by using larger state spaces
derived from Petri nets; and by distinguishing violated
formul\ae{} (for which testing automata fare better) from
verified formul\ae{} (where testing automata are hindered
by their two-pass emptiness check).}
}