Difference between revisions of "Publications/bensalem.15.lata"
From LRDE
| (10 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| published = true |
| published = true |
||
| − | | date = 2015- |
+ | | date = 2015-03-01 |
| authors = Ala Eddine Ben Salem |
| authors = Ala Eddine Ben Salem |
||
| title = Single-pass Testing Automata for LTL Model Checking |
| title = Single-pass Testing Automata for LTL Model Checking |
||
| Line 8: | Line 8: | ||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
| address = Nice, France |
| address = Nice, France |
||
| − | | |
+ | | volume = 8977 |
| − | | |
+ | | pages = 563 to 576 |
| − | | abstract = Testing Automaton (TA) is a new kind of |
+ | | abstract = Testing Automaton (TA) is a new kind of <math>\omega</math>-automaton introduced by Hansen et al. as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach. This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called Single-pass Testing Automaton (STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the "traditional" BA and TA approaches. These experiments show that STA compete well on our examples. |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.15.lata.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.15.lata.pdf |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| Line 18: | Line 18: | ||
@InProceedings<nowiki>{</nowiki> bensalem.15.lata, |
@InProceedings<nowiki>{</nowiki> bensalem.15.lata, |
||
author = <nowiki>{</nowiki>Ala Eddine Ben<nowiki>{</nowiki> S<nowiki>}</nowiki>alem<nowiki>}</nowiki>, |
author = <nowiki>{</nowiki>Ala Eddine Ben<nowiki>{</nowiki> S<nowiki>}</nowiki>alem<nowiki>}</nowiki>, |
||
| − | title = <nowiki>{</nowiki>Single-pass Testing Automata for LTL Model Checking<nowiki>}</nowiki>, |
+ | title = <nowiki>{</nowiki>Single-pass Testing Automata for <nowiki>{</nowiki>LTL<nowiki>}</nowiki> Model Checking<nowiki>}</nowiki>, |
booktitle = <nowiki>{</nowiki>Proceedings of the 9th International Conference on |
booktitle = <nowiki>{</nowiki>Proceedings of the 9th International Conference on |
||
Language and Automata Theory and Applications (LATA'15)<nowiki>}</nowiki>, |
Language and Automata Theory and Applications (LATA'15)<nowiki>}</nowiki>, |
||
| Line 25: | Line 25: | ||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
address = <nowiki>{</nowiki>Nice, France<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Nice, France<nowiki>}</nowiki>, |
||
| − | month = |
+ | month = mar, |
| + | volume = 8977, |
||
| − | + | pages = <nowiki>{</nowiki>563--576<nowiki>}</nowiki>, |
|
abstract = <nowiki>{</nowiki>Testing Automaton (TA) is a new kind of $\omega$-automaton |
abstract = <nowiki>{</nowiki>Testing Automaton (TA) is a new kind of $\omega$-automaton |
||
introduced by Hansen et al. as an alternative to the |
introduced by Hansen et al. as an alternative to the |
||
Latest revision as of 19:19, 5 January 2018
- Authors
- Ala Eddine Ben Salem
- Where
- Proceedings of the 9th International Conference on Language and Automata Theory and Applications (LATA'15)
- Place
- Nice, France
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2015-03-01
Abstract
Testing Automaton (TA) is a new kind of -automaton introduced by Hansen et al. as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach. This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called Single-pass Testing Automaton (STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the "traditional" BA and TA approaches. These experiments show that STA compete well on our examples.
Documents
Bibtex (lrde.bib)
@InProceedings{ bensalem.15.lata,
author = {Ala Eddine Ben{ S}alem},
title = {Single-pass Testing Automata for {LTL} Model Checking},
booktitle = {Proceedings of the 9th International Conference on
Language and Automata Theory and Applications (LATA'15)},
year = 2015,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
address = {Nice, France},
month = mar,
volume = 8977,
pages = {563--576},
abstract = {Testing Automaton (TA) is a new kind of $\omega$-automaton
introduced by Hansen et al. as an alternative to the
standard B\"uchi Automata (BA) for the verification of
stutter-invariant LTL properties. Geldenhuys and Hansen
shown later how to use TA in the automata-theoretic
approach to LTL model checking. They propose a TA-based
approach using a verification algorithm that requires two
searches (two passes) and compare its performance against
the BA approach. This paper improves their work by
proposing a transformation of TA into a normal form (STA)
that only requires a single one-pass verification
algorithm. The resulting automaton is called Single-pass
Testing Automaton (STA). We have implemented the STA
approach in Spot model checking library. We are thus able
to compare it with the "traditional" BA and TA approaches.
These experiments show that STA compete well on our
examples.}
}