@InProceedings{   poitrenaud.19.icfem,
  author        = {Denis Poitrenaud and Etienne Renault},
  title         = {Combining Parallel Emptiness Checks with Partial Order
                   Reductions},
  booktitle     = {Proceedings of the 21st International Conference on Formal
                   Engineering Methods (ICFEM'19)},
  editor        = {Yamine Ait Ameur and Shengchao Qin},
  address       = {Shenzhen, China},
  year          = 2019,
  month         = nov,
  pages         = {??--??},
  publisher     = {Springer},
  series        = {Lecture Notes in Computer Science},
  volume        = {11852},
  abstract      = { In explicit state model checking ofconcurrent systems,
                   multicore emptiness checks and partial order reductions
                   (POR) are two major techniques to handle large state
                   spaces. The first one tries to take advantage of
                   multi-core architectures while the second one may decrease
                   exponentially the size of the state space to explore.
                   For checking LTL properties, Bloemen and van de Pol [2] shown that
                   the best performance is currently obtained using their
                   multi-core SCC-based emptiness check. However, combining
                   the latest SCC-based algorithm with POR is not trivial
                   since a condition on cycles, the proviso, must be enforced
                   on an algorithm which processes collaboratively cycles. In
                   this paper, we suggest a pessimistic approach to tackle
                   this problem for liveness properties. For safety ones, we
                   propose an algorithm which takes benefit from the
                   information computed by the SCC-based algorithm. We also
                   present new parallel provisos for both safety and liveness
                   prop- erties that relies on other multi-core emptiness
                   checks. We observe that all presented algorithms maintain
                   good reductions and scalability.}
}