Leveraging polyhedral reductions for solving Petri net reachability problems

TL;DR

This paper introduces a novel polyhedral abstraction method using structural reductions and linear constraints to improve Petri net reachability analysis, implemented in the Kong tool and validated on diverse models.

Contribution

It presents a new polyhedral abstraction technique combined with a Token Flow Graph data structure for efficient reachability and concurrency analysis in Petri nets.

Findings

Effective on models from the Model Checking Contest

Works well with moderate reductions applied

Improves verification speed for Petri net reachability

Abstract

We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space abstraction, called polyhedral abstraction, which involves a combination between structural reductions and sets of linear arithmetic constraints between the marking of places. We propose a new data-structure, called a Token Flow Graph (TFG), that captures the particular structure of constraints occurring in polyhedral abstractions. We leverage TFGs to efficiently solve two reachability problems: first to check the reachability of a given marking; then to compute the concurrency relation of a net, that is all pairs of places that can be marked together in some reachable marking. Our algorithms are implemented in a tool, called Kong, that we evaluate 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.