Difference between revisions of "Publications/renault.16.sttt"
From LRDE
| Line 5: | Line 5: | ||
| title = Variations on Parallel Explicit Model Checking for Generalized Büchi Automata |
| title = Variations on Parallel Explicit Model Checking for Generalized Büchi Automata |
||
| journal = International Journal on Software Tools for Technology Transfer (STTT) |
| journal = International Journal on Software Tools for Technology Transfer (STTT) |
||
| + | | note = First published online on 26 April 2016. |
||
| − | | volume = xx |
||
| − | | |
+ | | volume = 19 |
| − | | |
+ | | number = 6 |
| + | | pages = 653 to 673 |
||
| publisher = Springer |
| publisher = Springer |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-10-26 |
| lrdenewsdate = 2015-10-26 |
||
| − | | abstract = We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness |
+ | | abstract = We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used. |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renault.16.sttt.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renault.16.sttt.pdf |
||
| type = article |
| type = article |
||
| Line 23: | Line 24: | ||
journal = <nowiki>{</nowiki>International Journal on Software Tools for Technology |
journal = <nowiki>{</nowiki>International Journal on Software Tools for Technology |
||
Transfer (STTT)<nowiki>}</nowiki>, |
Transfer (STTT)<nowiki>}</nowiki>, |
||
| − | year = |
+ | year = 2017, |
| + | note = <nowiki>{</nowiki>First published online on 26 April 2016.<nowiki>}</nowiki>, |
||
| − | volume = xx, |
||
| − | + | volume = 19, |
|
| − | + | number = 6, |
|
| + | pages = <nowiki>{</nowiki>653--673<nowiki>}</nowiki>, |
||
month = apr, |
month = apr, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
| Line 32: | Line 34: | ||
model checking. Unlike existing parallel emptiness checks, |
model checking. Unlike existing parallel emptiness checks, |
||
these are based on a Strongly Connected Component (SCC) |
these are based on a Strongly Connected Component (SCC) |
||
| − | enumeration, support generalized <nowiki>{</nowiki>B\"u<nowiki>}</nowiki> acceptance, and |
+ | enumeration, support generalized <nowiki>{</nowiki>B\"u<nowiki>}</nowiki>chi acceptance, and |
require no synchronization points nor recomputing |
require no synchronization points nor recomputing |
||
procedures. A salient feature of our algorithms is the use |
procedures. A salient feature of our algorithms is the use |
||
Revision as of 16:21, 5 February 2018
- Authors
- Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
- Journal
- International Journal on Software Tools for Technology Transfer (STTT)
- Type
- article
- Publisher
- Springer
- Projects
- Spot
- Date
- 2015-10-26
Abstract
We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.
Documents
Bibtex (lrde.bib)
@Article{ renault.16.sttt,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Variations on Parallel Explicit Model Checking for
Generalized {B\"u}chi Automata},
journal = {International Journal on Software Tools for Technology
Transfer (STTT)},
year = 2017,
note = {First published online on 26 April 2016.},
volume = 19,
number = 6,
pages = {653--673},
month = apr,
publisher = {Springer},
abstract = { We present new parallel explicit emptiness checks for LTL
model checking. Unlike existing parallel emptiness checks,
these are based on a Strongly Connected Component (SCC)
enumeration, support generalized {B\"u}chi acceptance, and
require no synchronization points nor recomputing
procedures. A salient feature of our algorithms is the use
of a global union-find data structure in which multiple
threads share structural information about the automaton
checked. Besides these basic algorithms, we present one
architectural variant isolating threads that write to the
union-find, and one extension that decomposes the automaton
based on the strength of its SCCs to use more optimized
emptiness checks. The results from an extensive
experimentation of our algorithms and their variations show
encouraging performances, especially when the decomposition
technique is used.}
}