Can Saturation Be Parallelised?

Abstract. Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other sequential symbolic state-space generators in that it exploits the locality of firing events in asynchronous system models. This paper explores whether event locality can be utilised to efficiently parallelise Saturation on shared-memory architectures. Conceptually, we propose to parallelise the firing of events within a decision diagram node, which is technically realised via a thread pool. We discuss the challenges involved in our parallel design and conduct experimental studies on its prototypical implementation. On a dual-processor dual-core PC, our studies show speed-ups for several example models, e.g., of up to 50% for a Kanban model, when compared to running our algorithm only on a single core.

• Type: Conference
• Year: 2006
• Where: FMICS
• Authors: Jonathan Ezekiel, Gerald Lüttgen, Radu Siminiceanu
• Keywords: FMICS 2006, Formal Methods, Saturation Algorithm, Sequential Symbolic State-space, Symbolic State-space Generators