Difference between revisions of "Publications/bensalem.14.tacas"
From LRDE
| Line 10: | Line 10: | ||
| pages = 440 to 454 |
| pages = 440 to 454 |
||
| address = Grenoble, France |
| address = Grenoble, France |
||
| − | | note = Accepted |
||
| urllrde = 2014-TACAS |
| urllrde = 2014-TACAS |
||
| abstract = In a previous work, we showed that a kind of ω-automata known as emphTransition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata. |
| abstract = In a previous work, we showed that a kind of ω-automata known as emphTransition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata. |
||
| Line 33: | Line 32: | ||
address = <nowiki>{</nowiki>Grenoble, France<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Grenoble, France<nowiki>}</nowiki>, |
||
month = apr, |
month = apr, |
||
| − | note = <nowiki>{</nowiki>Accepted<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki>In a previous work, we showed that a kind of |
abstract = <nowiki>{</nowiki>In a previous work, we showed that a kind of |
||
$\omega$-automata known as \emph<nowiki>{</nowiki>Tran\-sition-based |
$\omega$-automata known as \emph<nowiki>{</nowiki>Tran\-sition-based |
||
Revision as of 10:00, 28 November 2014
- Authors
- Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg
- Where
- Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)
- Place
- Grenoble, France
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2014-04-01
Abstract
In a previous work, we showed that a kind of ω-automata known as emphTransition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata.
Documents
Bibtex (lrde.bib)
@InProceedings{ bensalem.14.tacas,
author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
Fabrice Kordon and Yann Thierry-Mieg},
title = {Symbolic Model Checking of Stutter Invariant Properties
Using Generalized Testing Automata},
booktitle = {Proceedings of the 20th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'14)},
year = 2014,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8413,
pages = {440--454},
address = {Grenoble, France},
month = apr,
abstract = {In a previous work, we showed that a kind of
$\omega$-automata known as \emph{Tran\-sition-based
Generalized Testing Automata} (TGTA) can outperform the
B\"uchi automata traditionally used for \textit{explicit}
model checking when verifying stutter-invariant properties.
In this work, we investigate the use of these generalized
testing automata to improve \textit{symbolic} model
checking of stutter-invariant LTL properties. We propose an
efficient symbolic encoding of stuttering transitions in
the product between a model and a TGTA. Saturation
techniques available for decision diagrams then benefit
from the presence of stuttering self-loops on all states of
TGTA. Experimentation of this approach confirms that it
outperforms the symbolic approach based on
(transition-based) Generalized B\"uchi Automata.}
}