Compositionality of Some Behavioral Properties for Free-Choice Nested Petri Nets
Nested Petri nets (NP-nets) is an extension of Petri net formalism within the “nets-within-nets” approach, when tokens in a marking are Petri nets wich have autonomous behavior and synchronize with the system net. The formalism of NP-nets allows modeling multilevel multiagent systems with dynamic structure in a natural way. Currently there is no tool support for NP-nets simulation and analysis. The paper proposes translation of NP-nets into colored Petri nets and using CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.
Nested Petri nets (NP-nets) are Petri nets with net tokens - an extension of high-level Petri nets for modeling active objects, mobility and dynamics in distributed systems. In this paper we present an algorithm for translating two-level NP-nets into behaviorally equivalent Colored Petri nets with the view of applying CPN methods and tools for nested Petri nets analysis. We prove, that the proposed translation preserves dynamic semantics in terms of bisimulation equivalence.
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.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
Nested Petri nets (NP-nets) have proved to be one of the convenient formalisms for distributed multi-agent systems modeling and analysis. It allows representing multi-agent systems structure in a natural way, since tokens in the system net are Petri nets themselves, and have their own behavior. Multi-agent systems are highly concurrent. Verification of such systems with model checking method causes serious difficulties arising from the huge growth of the number of system intermediate states (state-space explosion problem). To solve this problem an approach based on unfolding system behavior was proposed in the literature. Earlier in  the applicability of unfolding for nested Petri nets verification was studied, and the method for constructing unfolding for safe conservative nested Petri nets was proposed. In this work we propose another method for constructing safe conservative nested Petri nets unfoldings, which is based on translation of such nets into classical Petri nets and applying standard method for unfolding construction to them. We discuss also the comparative merits of the two approaches.
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.
In this paper we examine how it is possible to control Petri net behavior with the help of transition priorities. Controlling here means forcing a process to behave in a stable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. For Petri net models stability is often ensured by liveness and boundedness. These properties are crucial in many application areas, e.g. workflow modeling, embedded systems design, and bioinformatics. In this paper we study the problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding priority constraints. We specify necessary conditions for the solvability of this problem and present an algorithm for ascribing priorities to net transitions in such a way that the resulting net becomes bounded while staying live.