Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets

TL;DR

This paper introduces an algorithm for safe Petri nets that identifies cliff-edge configurations, which are critical points where the system's evolution can irreversibly lead to undesirable states, using net unfoldings.

Contribution

It provides a novel unfolding-based method to find cliff-edge configurations in safe Petri nets, enhancing analysis of irreversible system behaviors.

Findings

The algorithm efficiently identifies all cliff-edge configurations.

It requires only a small prefix of the net unfolding, about twice Esparza's complete prefix.

The method improves understanding of long-term behaviors in concurrent systems.

Abstract

A crucial question in analyzing a concurrent system is to determine its long-run behaviour, and in particular, whether there are irreversible choices in its evolution, leading into parts of the reachability space from which there is no return to other parts. Casting this problem in the unifying framework of safe Petri nets, our previous work has provided techniques for identifying attractors, i.e. terminal strongly connected components of the reachability space, whose attraction basins we wish to determine. Here, we provide a solution for the case of safe Petri nets. Our algorithm uses net unfoldings and provides a map of all of the system's configurations (concurrent executions) that act as cliff-edges, i.e. any maximal extension for those configurations lies in some basin that is considered fatal. The computation turns out to require only a relatively small prefix of the unfolding, just twice the depth of Esparza's complete prefix.