Nested Petri Nets for Adaptive Process Modeling
We consider Nested Petri nets (NP-nets), i.e. Petri nets in which tokens can be Petri nets themselves. To increase flexibility and give tools for modeling adaptive processes we extend this formalism by allowing operations on net tokens. We prove decidabil
- PDF / 567,479 Bytes
- 15 Pages / 430 x 660 pts Page_size
- 37 Downloads / 228 Views
To my teacher B.A. Trakhtenbrot with sincere gratitude.
Abstract. We consider Nested Petri nets (NP-nets), i.e. Petri nets in which tokens can be Petri nets themselves. To increase flexibility and give tools for modeling adaptive processes we extend this formalism by allowing operations on net tokens. We prove decidability of some crucial for verification problems and thus show that, in spite of very flexible structure, NP-nets maintain “good” properties of ordinary Petri nets.
1
Introduction
Petri nets are a well-known formalism for modeling concurrent and distributed systems of less than Turing power. Limited expressiveness of Petri nets is more a merit, than a demerit, for many constitutive behavioral properties are decidable for Petri nets. In this paper we consider Nested Petri nets (NP-nets) [12,13,14,15,16,17] as a tool for adaptive modeling of concurrent and distributed processes. Informally speaking Nested Petri nets are Petri nets with net tokens, which may be generated, transferred, copied and removed as usual Petri net tokens. Net tokens may autonomously fire its inner transitions, thus changing their own marking. Net tokens may synchronize with one another (horizontal synchronization). There is also a mechanism of synchronizing transition firings in two adjacent levels (vertical synchronization). Vertical synchronization means simultaneous firing of a system net together with all net tokens “involved” in this firing. The idea of net tokens being Petri nets goes back to R. Valk [20], and “nets in nets” approach is extensively studied in the Petri net literature [1,10,11,18,21]. In all these works, the goal was to extend the expressive power or the expressive comfort of Petri nets, and, as a rule, this leads to Turing expressibility and undecidability of almost all interesting properties. For NP-nets it was proved, that though they are strictly more expressive than usual Petri nets (reachability is undecidable for NP-nets), they are still less
This research was partly supported by the Russian Foundation for Basic Research (grants 06-01-00106 and 07-01-00702).
A. Avron et al. (Eds.): Trakhtenbrot/Festschrift, LNCS 4800, pp. 460–474, 2008. c Springer-Verlag Berlin Heidelberg 2008
Nested Petri Nets for Adaptive Process Modeling
461
expressive than Turing machines and such problems as Termination, Coverability and some others are decidable for them. Here we extend nested Petri nets with operations on net tokens. Now in NPnets transition firing may transform involved net tokens and built new net tokens from the former ones by applying special net operations. This approach was already used in [4,5] for adaptive modeling of workflow processes. Nested workflow nets were defined there and decidability of soundness (proper termination – a crucial property for workflow modeling) was established. Now we consider in a certain sense more general situation – adaptive modeling for arbitrary processes, when net tokens represent some subprocesses and a system net controls their execution. Extending NP-nets with net oper
Data Loading...
