@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       = {??},
  number       = {??},
  pages        = {??--??},
  month        = apr,
  publisher    = {Springer},
  lrdeprojects = {Spot},
  lrdenewsdate = {2016-04-06},
  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.},
  lrdepaper    = {http://www.lrde.epita.fr/dload/papers/renault.16.sttt.pdf},
  lrdenewsdate = {2015-10-26}
}