Combining Parallel Emptiness Checks with Partial Order Reductions - Sorbonne Université
Communication Dans Un Congrès Année : 2019

Combining Parallel Emptiness Checks with Partial Order Reductions

Résumé

In explicit state model checking of concurrent systems, multi-core 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 properties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.
Fichier principal
Vignette du fichier
ICFEM19.pdf (375.2 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02408440 , version 1 (13-12-2019)

Identifiants

Citer

Denis Poitrenaud, Etienne Renault. Combining Parallel Emptiness Checks with Partial Order Reductions. ICFEM 2019 - 21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.370-386, ⟨10.1007/978-3-030-32409-4_23⟩. ⟨hal-02408440⟩
113 Consultations
95 Téléchargements

Altmetric

Partager

More