Towards parallel verification of concurrent systems using the Symbolic Observation Graph

An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG). Given a stutter-invariant event-based LTL formula phi, involving a subset of actions (called observable actions), the SOG is a condensed representation of the state space graph based on a symbolic encoding of the nodes (sets of states linked with unobservable actions) and an explicit representation of the edges (labelled with observable actions). It has the advantage to be much reduced comparing to the original state space graph while being equivalent with respect to stutter-invariant temporal properties (i.e., the original system satisfies phi if and only if the corresponding SOG satisfies phi). Aiming to go further in the process of tackling the state space explosion problem, we propose in this paper to parallelize the construction of the SOG using a hybrid approach (distributed+shared memory). Doing so, we take advantage of the recent advances in computer hardware, by distributing the construction process over a large number of multi-core processors. We studied the performances of our new approach comparing to both distributed and shared memory approaches on one side, and to the sequential construction on the other side. The obtained results show that the proposed approach offers an interesting alternative allowing to completely exploit the available distributed architecture while offering significant speedup.