Difference between revisions of "Publications/bensalem.14.tacas"
From LRDE
(Created page with "{{Publication | published = true | date = 2014-01-01 | authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg | title = Symbolic Model Checkin...") |
|||
Line 10: | Line 10: | ||
| pages = to be published |
| pages = to be published |
||
| address = Grenoble, France |
| address = Grenoble, France |
||
− | | note = Accepted |
+ | | note = Accepted |
+ | | urllrde = 2014-TACAS |
||
| abstract = In a previous work, we showed that a kind of ω-automata known as Transition-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 ̈uchi Automata. |
| abstract = In a previous work, we showed that a kind of ω-automata known as Transition-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 ̈uchi Automata. |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.14.tacas.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.14.tacas.pdf |
Revision as of 10:00, 29 January 2014
- Authors
- Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg
- Where
- 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
- Place
- Grenoble, France
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2014-01-01
Abstract
In a previous work, we showed that a kind of ω-automata known as Transition-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 ̈uchi 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 = {{20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}}, year = {2014}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {?}, pages = {to be published}, address = {Grenoble, France}, month = {April}, note = {Accepted}, 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üchi 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.} }