Checking marking reachability with the state equation in Petri net subclasses

TL;DR

This paper identifies subclasses of weighted Petri nets where reachability can be efficiently checked using linear algebra, by establishing conditions for the PR-R equality that simplifies analysis.

Contribution

It delineates new subclasses of weighted Petri nets where the set of reachable markings equals the potentially reachable set, enabling algebraic reachability analysis.

Findings

PR-R equality holds in certain subclasses of weighted Petri nets.

Conditions are provided for when the set of reachable markings equals the potential set.

The approach extends to more expressive classes, including those with shared buffers.

Abstract

Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In order to alleviate this difficulty, various structural and behavioral restrictions have been considered, allowing to relate reachability to properties that are easier to check. For a given initial marking, the set of potentially reachable markings is described by the state equation solutions and over-approximates the set of reachable markings. In this paper, we delineate several subclasses of weighted Petri nets in which the set of reachable markings equals the set of potentially reachable ones, a property we call the PR-R equality. When fulfilled, this property allows to use linear algebra to answer the reachability questions, avoiding a brute-force analysis of the state space. Notably, we provide conditions under which this equality holds in classes much more expressive than marked graphs, adding places with several ingoing and outgoing transitions, which allows to model real applications with shared buffers. To achieve it, we investigate the relationship between liveness, reversibility, boundedness and potential reachability in Petri nets. We also show that this equality does not hold in classes with close modeling capability when the conditions are relaxed.