Accelerating the Computation of Dead and Concurrent Places using Reductions

TL;DR

This paper introduces a novel method combining structural reductions and linear algebra to accelerate the computation of concurrency relations in Petri nets, implemented in the Kong tool and tested on diverse models.

Contribution

The paper presents a new approach using state space abstraction and a specialized data structure to improve the efficiency of computing concurrency in Petri nets.

Findings

Effective acceleration of concurrency computation demonstrated.

Works well with moderate reductions on real models.

Implementation in the Kong tool shows practical applicability.

Abstract

We propose a new method for accelerating the computation of a concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on a state space abstraction, that involves a mix between structural reductions and linear algebra, and a new data-structure that is specifically designed for our task. Our algorithms are implemented in a tool, called Kong, that we test on a large collection of models used during the 2020 edition of the Model Checking Contest. Our experiments show that the approach works well, even when a moderate amount of reductions applies.