Difference between revisions of "Publications/renault.15.tacas"
From LRDE
(Created page with "{{Publication | published = true | date = 2015-01-13 | authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud | title = Parallel Explicit Model Chec...") |
|||
(8 intermediate revisions by the same user not shown) | |||
Line 6: | Line 6: | ||
| booktitle = Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15) |
| booktitle = Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15) |
||
| editors = Christel Baier, Cesare Tinelli |
| editors = Christel Baier, Cesare Tinelli |
||
− | | |
+ | | pages = 613 to 627 |
− | | pages = XX to XX |
||
| publisher = Springer |
| publisher = Springer |
||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
− | | volume = |
+ | | volume = 9035 |
| abstract = We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair 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 being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments. |
| abstract = We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair 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 being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments. |
||
− | | |
+ | | lrdepaper = http://www.lrde.epita.fr/dload/papers/renault.15.tacas.pdf |
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-01-13 |
| lrdenewsdate = 2015-01-13 |
||
| type = inproceedings |
| type = inproceedings |
||
| id = renault.15.tacas |
| id = renault.15.tacas |
||
+ | | identifier = doi:10.1007/978-3-662-46681-0_56 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> renault.15.tacas, |
@InProceedings<nowiki>{</nowiki> renault.15.tacas, |
||
Line 29: | Line 29: | ||
year = 2015, |
year = 2015, |
||
month = apr, |
month = apr, |
||
− | + | pages = <nowiki>{</nowiki>613--627<nowiki>}</nowiki>, |
|
− | pages = <nowiki>{</nowiki>XX--XX<nowiki>}</nowiki>, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
− | volume = |
+ | volume = 9035, |
abstract = <nowiki>{</nowiki>We present new parallel emptiness checks for LTL model |
abstract = <nowiki>{</nowiki>We present new parallel emptiness checks for LTL model |
||
checking. Unlike existing parallel emptiness checks, these |
checking. Unlike existing parallel emptiness checks, these |
||
Line 45: | Line 44: | ||
better speedup than existing algorithms in half of our |
better speedup than existing algorithms in half of our |
||
experiments.<nowiki>}</nowiki>, |
experiments.<nowiki>}</nowiki>, |
||
− | + | doi = <nowiki>{</nowiki>10.1007/978-3-662-46681-0_56<nowiki>}</nowiki> |
|
− | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 11:30, 1 April 2019
- Authors
- Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
- Where
- Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2015-01-13
Abstract
We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair 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 being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.
Documents
Bibtex (lrde.bib)
@InProceedings{ renault.15.tacas, author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice Kordon and Denis Poitrenaud}, title = {Parallel Explicit Model Checking for Generalized {B\"u}chi Automata}, booktitle = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15)}, editor = {Christel Baier and Cesare Tinelli}, year = 2015, month = apr, pages = {613--627}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 9035, abstract = {We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair 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 being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.}, doi = {10.1007/978-3-662-46681-0_56} }