A Toolchain to Compute Concurrent Places of Petri Nets
Abstract
The concurrent places of a Petri net are all pairs of places that may
simultaneously have a token in some reachable marking. Concurrent places
generalize the usual notion of dead places and are particularly useful for
decomposing a Petri net into synchronized automata executing in parallel.
We present a state-of-the-art toolchain to compute the concurrent places of
a Petri net. This is achieved by a rich combination of various techniques,
including: state-space exploration using BDDs, structural rules for concurrent
places, quadratic over- and under-approximation of reachable markings, and
polyhedral abstraction of the state space based on structural reductions and
linear arithmetic constraints on markings. We assess the performance of our
toolchain on a large collection of 850 nets originating from the 2022
edition of the Model Checking Contest.
