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...")
 
 
(6 intermediate revisions by the same user not shown)
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 = ??
  
−
| number = ??
 +
| volume = 19
−
| pages = ?? to ??
 +
| 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 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.
 +
| abstract = We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checksthese 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
 
| id = renault.16.sttt
  
| id = renault.16.sttt
  +
| identifier = doi:10.1007/s10009-016-0422-5
 
| bibtex =
 
| bibtex =
 
@Article<nowiki>{</nowiki> renault.16.sttt,
  
@Article<nowiki>{</nowiki> renault.16.sttt,
Line 23: Line 25:
 
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 = 2016,
 +
year = 2017,
−
volume = <nowiki>{</nowiki>??<nowiki>}</nowiki>,
 +
note = <nowiki>{</nowiki>First published online on 26 April 2016.<nowiki>}</nowiki>,
  ⚫
volume = 19,
⚫
number = <nowiki>{</nowiki>??<nowiki>}</nowiki>,
  
  +
number = 6,
⚫
pages = <nowiki>{</nowiki>??--??<nowiki>}</nowiki>,
  
  ⚫
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 35:
 
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
Line 44: Line 47:
 
experimentation of our algorithms and their variations show
  
experimentation of our algorithms and their variations show
 
encouraging performances, especially when the decomposition
  
encouraging performances, especially when the decomposition
−
technique is used.<nowiki>}</nowiki>
 +
technique is used.<nowiki>}</nowiki>,
  ⚫
doi = <nowiki>{</nowiki>10.1007/s10009-016-0422-5<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
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 checksthese 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.},
  doi		= {10.1007/s10009-016-0422-5}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/renault.16.sttt&oldid=123243"