Difference between revisions of "Publications/renault.16.sttt"
From LRDE
(Created page with "{{Publication | published = true | date = 2015-10-26 | authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud | title = Variations on Parallel Expli...") |
|||
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) |
||
− | | volume = |
+ | | volume = xx |
− | | number = |
+ | | number = x |
− | | pages = |
+ | | pages = xx to x |
| publisher = Springer |
| publisher = Springer |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
Line 24: | Line 24: | ||
Transfer (STTT)<nowiki>}</nowiki>, |
Transfer (STTT)<nowiki>}</nowiki>, |
||
year = 2016, |
year = 2016, |
||
− | volume = |
+ | volume = xx, |
− | number = |
+ | number = x, |
− | pages = |
+ | pages = xx--x, |
month = apr, |
month = apr, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
Revision as of 10:42, 8 April 2016
- 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) enumerationsupport generalized Bü 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-findand 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 = 2016, volume = xx, number = x, pages = xx--x, 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} 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.} }