Greetings,
We are please to announce that the following paper has been accepted in 21st International
Conference on Formal Engineering Methods (ICFEM'19). Please find the title and
abstract below.
Title and corresponding authors:
"Combining Parallel Emptiness Checks with Partial Order Reductions"
Denis Poitrenaud (1,2) and Etienne Renault (3)
(1) Sorbonne Université, CNRS, LIP6, F-75005 Paris, France
(2) Université Paris Descartes, Paris, France
(3) LRDE, Epita, Paris, France
Abstract:
In explicit state model checking of concurrent 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.
More information at :
https://www.lrde.epita.fr/wiki/Publications/renault.18.vecos
<https://www.lrde.epita.fr/wiki/Publications/renault.18.vecos>