A Necessary and Sufficient Condition for the Liveness and Reversibility of Process-Resource Nets With Acyclic, Quasi-live, Serializable, and Reversible Process Subnets

The first part of this paper develops a linear characterization for the space of the Petri net markings that are reachable from the initial marking M₀ through bounded-length fireable transition sequences. The second part discusses the practical implications of this result for the liveness and reversibility analysis of a particular class of Petri nets known as process-resource nets with acyclic, quasi-live, serializable, and reversible process subnets. Note to Practitioners-One of the main challenges in the analysis and design of the resource allocation taking place in modern technological systems is the verification of certain properties of the system behavior such as liveness and deadlock freedom. The last decade has seen the development of a number of computational tests that can evaluate the aforementioned properties for a large class of resource allocation systems. The tests that are most promising essentially verify the target properties by establishing the absence of some undesirable structure from the states that are reachable during system operation. As a result, the effective execution of these tests necessitates the effective representation of the underlying reachability space. Yet, in the past, the development of a concise and computationally manageable representation of the system reachability space has been considered to be a challenging proposition and a factor that compromises the resolution power of the aforementioned tests. The work presented in this paper establishes that for a very large class of the considered resource allocation systems, the underlying reachability space admits a precise and computationally efficient characterization, which subsequently leads to more powerful verification tools of the target behavioral properties