Towards Distributed Verification of Petri Nets Properties

The use of distributed or parallel processing gained interest in the recent years to fight the state space explosion problem. Many industrial systems are described with large models, and the state space being even larger, it does not fit completely into the memory of a single computer. In this approach several computers connected over a network cooperate. The state space is then partitionned among these computers, and each of them contributes to the verification by considering its own subspace. In this paper, we address the verification of basic behavioural properties: reachability, liveness and home state and their distributed analysis. In particular, the verification of the latter properties requires the generation of the full state space and the computation of its terminal strongly connected components. Here, we propose to use a distributed Tarjan algorithm to perform this computation. The performance of distributed verification depends on several criteria, e.g. load balancing of the partitionned state space, but also more importantly on a good partitioning. Therefore, choosing an adequate hash function to assign nodes to processors is important.