Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level Nested Petri nets (NP-nets). Boundedness and liveness are still very hard to check even for plain Petri nets (EXPSPACE or worse). For the restricted class of free-choice Petri nets some problems become more amenable to analysis. There is the polynomial time algorithm to check if a free-choice Petri net is live and bounded. We prove that for some restricted class of NP-nets with free-choice components boundedness can be checked in a compositional way and define restrictions, under which liveness is also compositional. The motivating example of such restricted NP-nets is provided.
This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017.
The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, with 1 short abstract and 3 extended abstracts of invited talks presented together in this volume were carefully reviewed and selected from 33 submissions. The focus of the conference is on following topics: Simulation of Colored Petri Nets, Petri Net Tools.- Model Checking, Liveness and Opacity, Stochastic Petri Nets, Specific Net Classes, and Petri Nets for Pathways.
In this paper we examine how it is possible to control Petri net behavior with the help of time constraints. Controlling here means to force a process to behave in a desirable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. Liveness and boundedness are crucial properties in many application areas, e.g. workflow modeling and bioinformatics. The main correctness property for workflow models is soundness, which can be reduced to the liveness and boundedness of a modified net. In biological models, liveness and boundedness are important for system stability. The problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding priority constraints is studied in this paper. We specify necessary conditions for the solvability of this problem and present a method for ascribing priorities to net transitions in such a way that the resulting net becomes bounded while staying live.