Download PDFOpen PDF in browser

Branching Processes of Conservative Nested Petri Nets

17 pagesPublished: July 28, 2014


Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the “nets-within-nets” approach, when tokens in a marking are themselves Petri nets which have autonomous behavior and synchronize with the system net. The formalism of NP- nets allows modeling multi-level multi-agent systems with dynamic structure in a natural way. In this paper we define branching processes and unfoldings for conservative NP- nets, i.e. for NP-nets with a persistent set of agents. We prove that NP-nets unfoldings satisfy the fundamental property of unfoldings, and thus can be used for verification of conservative NP-nets in line with classical unfolding methods.

Keyphrases: petri nets, true concurrency, unfoldings, nested petri nets

In: Alexei Lisitsa and Andrei Nemytykh (editors). VPT 2014. Second International Workshop on Verification and Program Transformation. EPiC Series in Computing, vol 28, pages 19-35

Download PDFOpen PDF in browser