Petri Nets of Active Resources (AR-nets) represent a dual syntax of Petri nets with a single type of nodes (places and transitions are united) and two types of arcs (input and output arcs are separated). In AR-nets the same token may be considered as a passive resource (produced or consumed by agents) and an active agent (producing or consuming resources) at the same time. It is shown that the homogeneous structure of nodes in AR-nets allows some specific modular modeling and transformation techniques. Properties of net partitions and reachability-equivalent module replacements are studied.
Nowadays there exist a lot of Petri net modifications introducing different
modular and/or hierarchical syntax. In particular, different high-level formalisms
appeared to be quite effective and useful in practice [
As a rule, in compositional Petri nets modules may be linked by synchronized
transitions [
However, explicit separation of nodes into places and transitions is not the
only way of Petri net definition. There exists a number of equivalent formalisms
with a different separation of elements. Some of them use the duality between
places and transitions (the importance of studying this duality was mentioned
by C.-A.Petri already in [
In [
In [
In both dual P/T nets and Super-Dual nets duality is based on two types of
elements of the system — resources and actions (places and transitions). These
elements are represented in the net by vertices of a bipartite oriented graph.
However, there is another (implicitly) divided set in every Petri net (and in
every other bipartite oriented graph) — the set of arcs. It contains arcs of two
crucially different types — input arcs from places to transitions remove tokens,
output arcs from transitions to places produce tokens. The explicit separation of
this notions allowed us to define an “orthogonal” syntax for Petri nets — Nets
of Active Resources (AR-nets) [
A definition of an AR-net is a dualized definition of a Petri net. The set of
arcs is explicitly transformed into two separate sets of input arcs and output
arcs. The sets of transitions and places are united into a single set of nodes.
Each node may contain tokens. A token in the node may fire, consuming some
tokens through input arcs and producing some other tokens through output arcs.
So a token simulates behaviour of both an active component (an agent) and a
passive component (a resource) at the same time. Therefore the formalism is
called “nets of active resources”. AR-nets are well-suited for modeling systems
with an explicit definition of an agent [
In this paper we study the compositional properties of AR-nets. A module is represented as a subnet defined by some subset of nodes. An interface of the module is a set of arcs linking its nodes with an outer subnet. A module may have four types of links: input, output, production and consumption. First two of them represent actions of the module itself, the other two represent actions of its neighbours. Hence syntactically a module with adjacent links can be treated as a node with adjacent arcs. This generalization is quite natural and does not affects the homogeneity of the graph of the net.
It is shown that a number of net properties may be inherited from the properties of modules of particular types. It is proven that any nested decomposition of the net can be transformed into an equivalent agent/resource decomposition. For a flat decomposition these kinds of transformations are applicable depending only on the chromatic number of the module linkage graph.
A problem of module equivalence w.r.t. system reachability is also defined and studied. A most general case of this equivalence is obviously undecidable. For a simple case of replacement a criterion of equivalence is given. It is shown how a module (with some additional requirements) can be replaced by a single node without affecting the global reachability relation.
The paper is organized as follows. In section 2 we give basic definitions and notations for nets of active resources. In section 3 an AR-module is introduced. We study different types of modules, their properties and methods of decompositions. In section 4 two notions of module equivalence are defined and studied. Section 5 contains some conclusions and directions for possible future work. 2
Let S be a finite set. A multiset M over a set S is a mapping M : S → Nat, where Nat is the set of natural numbers (including zero), i. e. a multiset may contain several copies of the same element.
For two multisets M, M 0 we write M ⊆ M 0 iff ∀s ∈ S : M (s) ≤ M 0(s) (the inclusion relation). The sum and the union of two multisets M and M 0 are defined as usual: ∀s ∈ S : (M +M 0)(s) = M (s)+M 0(s), M ∪M 0(s) = max(M (s), M 0(s)).
By M(S) we denote the set of all finite multisets over S.
For a multiset M ∈ M(S) and a subset S0 ⊆ S denote a projection M [S0] ∈ M(S0) of M onto S0 as follows: ∀s ∈ S0 : M [S0](s) = M (s).
Similarly, for a binary relation R ⊆ M(S) × M(S) a projection R[S0] ⊆
M(S0)×M(S0) is defined as follows: ∀s1, s2 ∈ S0 (s1, s2) ∈ R[S0] ⇔ (s1, s2) ∈ R.
Definition 1. [
In graphic form the nodes are represented by circles, the consumption relation by dotted arrows and the production relation by solid arrows.
A marked net of active resources is a pair (N, M0) where N is an AR-net and M0 ∈ M(V ) is its initial marking.
As usual, pictorially the marking is denoted by black dots.
For a node v ∈ V by I(•, v), O(v, •), I(v, •) and O(•, v) denote the multisets of nodes of preconditions, postconditions, consumers and producers: ∀w ∈ V I(•, v)(w) =def I(w, v); I(v, •)(w) =def I(v, w);
O(v, •)(w) =def O(v, w); O(•, v)(w) =def O(w, v).
Definition 2. A node v ∈ V is active in a marking M iff – M (v) > 0 (the node v is not empty); – I(•, v) ⊆ M (there are enough tokens in all its input nodes). An active node v may fire yielding a new marking M 0 s.t.
M 0 =def M − I(•, v) + O(v, •) (denoted M →v M 0).
Some natural notions:
Let i ∈ I and i = (v1, v2). Then the arc i is called an input arc for the node v2 and a consuming arc for the node v1. A token in the node v1 may be consumed through the arc i, a token in the node v2 can consume through the arc i.
Let o ∈ O and o = (v1, v2). Then the arc o is called an output arc for the node v1 and a producing arc for the node v2. A token in the node v1 can produce through the arc o, a token in the node v2 may be produced through the arc o.
It is impossible to define consuming output and producing input. The token may be producing, consuming, produced and consumed at the same time (through different incident arcs). It can be even self-copied (by producing loop) or self-consumed (by consuming loop).
An example of an AR-net is given on Fig. 1(a). Here we model a system, containing three processes that request two shared resources. Processes are modeled by tokens in the nodes ready-to-start and ready-to-stop, access keys – by tokens in the node keys. The model guarantees that at most two processes can work with resources at the same time. An example of a sequence of firings is given on Fig. 2 (here r1 denotes ready-to-start and r2 denotes ready-to-stop).
On Fig. 1(b) an equivalent Petri net is also presented. Note the difference between two nets. In AR-net the more simple node structure and the more complex arc structure allowed us to use the same node of the graph as a model for both place and transition. For example, the node ready-to-start is a replacement for both place waiting and transition start. Its tokens produce other tokens (in ready-to-stop) and are produced by other tokens (by ready-to-stop). They also consume other tokens (from keys) and are self-consumed (through the loop).
The notion of firing is extended to sequences in the standard way: for σ ∈ V ∗ s.t. σ = σ0v with v ∈ V we say that M →σ M 0 iff M →σ0 M 00 →v M 0 for some M 00.
A set of reachable markings is defined as follows: σ
R(N, M0) =def {M ∈ M(V ) | ∃σ ∈ T ∗ : M0 → M }.
A node v is live in a marked net (N, M0) iff for any M ∈ R(N, M0) there exists M 0 ∈ R(N, M ) such that v is active in M 0. A marked net is live iff all its nodes are live.
The reachability relation is defined as follows:
The syntax of AR-nets substantially differs from the syntax of Petri nets. It
may be considered dual: instead of two types of vertices and a single type of arcs
we use a single type of vertices and two types of arcs. However, AR-nets define
the same class of systems and hence represent yet another variant of Petri net
formalism:
Theorem 1. [
The proof of AR→PN transformation is based on the method, proposed in
[
Let N = (V, I, O) be an AR-net. A module μ of the net N is defined by some subset of nodes Vμ ⊆ V (considered as internal nodes of the module).
For a module μ of N denote: 1 For each AR-net there exists a Petri net with the same reachability and vice versa. – Iμ = {(v, v0) ∈ I | v, v0 ∈ Vμ} – internal input arcs; – Oμ = {(v, v0) ∈ O | v, v0 ∈ Vμ} – internal output arcs; – Nμ = (Vμ, Iμ, Oμ) – a net of the module μ; – Aiμ = {(v, v0) ∈ I | v ∈ (V \ Vμ), v0 ∈ Vμ} – input links; – Aoμ = {(v, v0) ∈ O | v ∈ Vμ, v0 ∈ (V \ Vμ)} – output links; – Rμi = {(v, v0) ∈ I | v ∈ Vμ, v0 ∈ (V \ Vμ)} – consuming links; – Rμo = {(v, v0) ∈ O | v ∈ (V \ Vμ), v0 ∈ Vμ} – producing links.
Informally, A-links represents the observable activity of the module, R-links describe its role as a resource.
For a marked net (N, M0) and a module μ a marked net of the module (Nμ, (M0)μ) is defined straightforwardly: (M0)μ =def M0[Vμ].
Define also a complement μ of the module μ as a module, defined by a subset of nodes V \ Vμ. A complement of the module may be considered as a system subnet of the net.
A well-known model of dining philosophers is given on Fig. 5. For the sake of simplicity we consider only two participants. A module is defined representing the first philosopher. Note that it has only input and output links (elements of Aiμ and Aoμ), so the module may be considered as a pure agent.
A module in an AR-net has almost the same external appearance as a single node: it may consume and produce resources of other modules, and its own resources may be consumed and produced by other modules. Moreover, the relations between modules are naturally denoted by the same constructive elements as at the underlying level of nodes: input and output arcs (links). Hence, the induced hierarchical syntax is quite compact.
Modules having not all four types of links are of a particular interest. We will call a module μ an A-module (resp. R-module) if it has only A-links (resp. R-links). For example, the philosopher1 is an A-module. Modules with a more restricted interfaces will be denoted using appropriate superscripts: for example, AiRo-module has only input and producing links.
Any AR-net may be considered as a composition of modules of different types (Fig. 6). Here are several trivial properties of some of these types: Proposition 1. Let (N, M0) be a marked net and μ be a module of N . Then 1. (Nμ, (M0)μ) is unbounded and μ is an AoR-module ⇒ (N, M0) is unbounded; 2. (Nμ, (M0)μ) is not live and μ is an ARi-module ⇒ (N, M0) is not live; 3. (Nμ, (M0)μ) is live and μ is an Ao-module ⇒ (Nμ, (M0)μ) is unbounded. Proof. 1. Since there are no input links, the behavior of the active nodes of the module does not depend on the marking of the system part of the net. Therefore we can take an unbounded run of the module as an unbounded run of the whole net. 2. The ARi-module cannot obtain any additional tokens from the outside (there are no producing links). So its nodes are not live in the whole net too. 3. Obviously, the live module with only output external links sends the unbounded number of tokens to the outside.
Among all 11 possible types of modules pure A- and R-modules (agents and resources) are the most important. Any interface between two modules may be transformed into an equivalent2 A/R interface with one module being an agent, and the other being a resource. Consider a simple procedure transforming input and output links into producing and consuming links: Lemma 1. Let (N, M0) be a marked AR-net and v ∈ V be a node such that I(•, v) 6= ∅ or O(v, •) 6= ∅ ( v is active: it can consume or produce tokens).
Let N 0 be a net, constructed from N by removing all arcs, participating in I(•, v) and O(v, •) ( v became passive), and adding a new node vt with I(vt, •) = O(•, vt) = ∅ ( vt cannot be produced or consumed), I(•, vt) = I(•, v) ∪ {(v, vt)}, O(vt, •) = O(v, •) ∪ {(vt, v)} ( vt simulate in N 0 the firing of v in N ).
Let M00 be a marking of N 0 such that M00 [V ] = M0, M00 (vt) = 1. Then Reach(N, M0) = Reach(N 0, M00 ) ∩ (V ×V ) and ∀M 0 ∈ R(N 0, M00 ) M 0(vt) = 1. Proof. The illustration of such a transformation is given on Fig. 7.
The proof is straightforward – all possible links of a node are considered. Actually, we just separated active and passive properties of node v (just like in Fig. 3). The new node vt is a transition: it behaves completely like an ordinary Petri net transition. Similarly, the node v in N 0 is a Petri net place.
The restructuring, described in Lemma 1, extends the set of nodes by a transition, always marked by a single token. So we do not take this node into account when considering the reachability set of the new net.
Corollary 1. 1) Any module of an AR-net may be transformed into R-module without changing the reachability set of the net; 2) Any module of an AR-net may be transformed into A-module without changing the reachability set of the net. 2 (w.r.t. reachability) μ μ μ μ
Proof. (1) Any active node v of the module, having an external link, is replaced by a pair (v, vt) of a place and a transition. The new transitions are put outside of the module (Fig. 7).
(2) A dual transformation: active nodes of the system part are transformed, transitions are put into the module.
So the interface of any module can be simplified to R-interface or A-interface. Of course, doing this we change the structure of the net (vt is added). However, this modification is local and does not affect the “inner” part of the module.
In practice A- and R-modules may be considered as “active” and “passive” parts of the system (“control” and “data”). Corollary 1 states that the separation is “relative”: we can easily modify an agent to be a resource and vice versa. This duality is quite trivial in modular AR-nets.
Definition 3. A flat modularization Ω of a net N is a partition of V into non-intersecting modules {μ1, . . . , μn}.
A flat modularization is called a flat A/R-modularization iff every module is either A-module or R-module.
Corollary 2. Let Ω = {μ1, . . . , μn} be a flat modularization of N . Let G be a graph with vertices from Ω, such that two vertices μi and μj are connected in G iff there is an arc between modules μi and μj in N .
The net N may be transformed into an equivalent (w.r.t. reachability) net N 0 such that Ω is an A/R-modularization of N 0 iff the chromatic number of G is 2. Proof. Modules of one color are transformed into A-modules, of another – into R-modules.
Corollary 2 states that any two-color partition of the net can be transformed to an active/passive partition. Hence we can easely identify control and data structures, corresponding to the given partition: control modules sharing the same data, data modules sharing the same control, chains of linked modules etc. Moreover, control and data subnets are dualizable (Corollary 1). Definition 4. A nested modularization Ω of a net N is a partition of V into a module μ and a system part μ, where μ may also be modularized.
A nested modularization is called a nested A/R-modularization / A-modularization / R-modularization iff every module is either A- or R-module / Amodule / R-module.
Corollary 3. For any nested modularization Ω of N this net may be transformed into an equivalent (w.r.t. reachability) net N 0 such that Ω is a nested α-modularization of N 0 (α ∈ {A/R,A,R}).
Proof. Straightforward. The transformation (if required) must be started from the innermost module.
The nested modularization allows us to construct a hierarchical structure with any kind of inter-level communication. The combinations of flat and nested modularizations are also possible.
A/R-modularizations are interesting because they allow to incorporate a natural hierarchy into the set of modules. Such hierarchy may have many applications in extended formalisms. For example, active modules may be considered responsible for intermodular data transfer. Another example is security: the Rmodule is able to hide the exact moments of its transition firings from the agent (the A-module), because agent observes only the already changed state of the resource. 4
In this section we consider equivalent modules. The key problem is to check whether a particular module can be replaced by another one without harming the behaviour of the whole system. We study the equality of reachability relations of two nets – a fundamental behavioural equivalence, which is stronger than language equivalence and bisimulation.
Definition 5. Consider AR-nets N1 and N2 and modules μ1 and μ2 of N1 and N2 respectively, such that (N1)μ1 = (N2)μ2 = Nsys for some AR-net Nsys = (Vsys, Isys, Osys) (a same system net). Consider markings M1, M2 and Msys of μ1, μ2 and Nsys respectively.
Marked modules (μ1, M1) and (μ2, M2) are called equivalent w.r.t. system reachability for a marked system net (Nsys, Msys) (SR-equivalent for short) iff
Reach(N1, M1 + Msys)[Vsys] = Reach(N2, M2 + Msys)[Vsys].
Informally, two SR-equivalent modules have the same effect on the system part of the net. They can be replaced by each other without harming the system’s reachability set.
An example is given on Fig. 10. The module Philosopher’ is SR-equivalent to the module Philosopher1, shown on Fig. 5. Note that these modules are different: Philosopher’ has additional state ready, in which it has both forks but is not eating.
Theorem 2. SR-equivalence is undecidable for general AR-nets. Proof. Follows from the undecidability of R-equivalence for general Petri nets (a problem of deciding whether two nets have the same reachability set). Indeed, one can put all “agent nodes” (“transitions”) of compared nets into corresponding modules (and all “resource nodes” aka “places” into system nets) and try to check their SR-equivalence.
Note that in the proof we used active modules (A-modules). Hence SRequivalence is undecidable even for A-modules. It may be interesting to study the equivalence for other specific types of modules, in particular, for R-modules. We believe that it is undecidable as well.
Consider a more restricted case of a module. Let both modules have the same interface, i.e. the same set of links and adjacent nodes in the system net: ∀v ∈ Vsys
P v1∈Vμ1
P v1∈Vμ1
Aoμ1 (v1, v) = Aiμ1 (v, v1) =
P v2∈Vμ2
P v2∈Vμ2
Aoμ2 (v2, v); Aiμ2 (v, v2);
P v1∈Vμ1
P v1∈Vμ1
Rμi1 (v1, v) = Rμo1 (v, v1) =
P v2∈Vμ2
P v2∈Vμ2
Rμi2 (v2, v); Rμo2 (v, v2).
We will say that a module is compatible with a system net (and vice versa) iff the net contains nodes required by all links of the module.
Definition 6. Marked modules (μ1, M1) and (μ2, M2), having the same interface, are called universally equivalent w.r.t. system reachability (USR-equivalent for short) iff they are SR-equivalent for any compatible marked system net.
The USR-equivalence of two modules means that they produce equal sets of markings on passive interface nodes (by active agent links) and obey the same sets of restrictions and commands, coming from active interface nodes (by passive resource links).
A USR-equivalence is a restriction of an SR-equivalence. However, we believe that it is also undecidable.
Consider one of the simplest nontrivial module replacement – let the first module (denoted by μ) be a general AR-net (with some restrictions) and the second one (denoted by ν) be a single node.
Theorem 3. Let (μ, M ) be a marked module s.t. 1. All active interface nodes of module μ have the same multisets of active links: ∃Ai, Ao ∈ M(Vsys) ∀v ∈ Vμ (Aiμ(•, v) = Aoμ(v, •) = ∅) ∨ (Aiμ(•, v) = Ai ∧ Aoμ(v, •) = Ao). 2. All active interface nodes of system net perform operations on the whole numbers of the same multiset of internal nodes:
∃Rio ∈ M(Vμ) ∀v ∈ Vsys ∃ki(v), ko(v) ∈ Nat (Rμi(•, v) = ki(v) × Rio ∧ Rμo(v, •) = ko(v) × Rio). 3. All active internal nodes of the module, affecting nodes of Rio, perform the same operation on the whole numbers of Rio’s: ∃kc, kp ∈ Nat
∀v ∈ Vμ (Aiμ(•, v) ∩ Rio 6= ∅ ∨ Aoμ(v, •) ∩ Rio 6= ∅) ∃X, Y ∈ M(Vμ) (X ∩ Rio = Y ∩ Rio = ∅) ∧ (Aiμ(•, v) = kc × Rio + X) ∧ (Aoμ(v, •) = kp × Rio + Y ) . ⇒ 4. The initial marking M may be decomposed as M = M 0 + m × Rio, where m ∈ Nat and M 0 ∩ Rio = ∅. 5. The marked internal net (Nμ, M ) is live, were M denotes a marking, produced from M by emptying all passive interface nodes of μ : ∀v ∈ Vμ
M (v) =def 0 M (v) if (Aiμ(•, v) ∪ Aoμ(v, •)) 6= ∅; otherwise.
Then (μ, M ) is USR-equivalent to a marked single-node module (ν, Mν ), where – Vν = {w}; – Iν (w, w) = kc; Oν (w, w) = kp; – Aiν (•, w) = Ai; Aoν (w, •) = Ao; – ∀v ∈ Vsys Rνi (w, v) = ki(v), Rνo (v, w) = ko(v); – Mν (w) = m.
Proof. The proof is technical. It is based on the fact that the liveness of the “unmarked” module implies the liveness of any node of the module in any bigger initial marking (such a marking may be obtained by input from the system). The system does not depend on the actual behaviour of the internal net (note that the effect of all interface firings is the same). It is enough to know that any firing is eventually possible.
An example of correct replacement is given on Fig. 11.
Here the module Procedure (live and unbounded) models some computation, that may be performed by one of three computers, initially positioned in the node idle. The service loader starts the computation, loading one of the computers with an input data. The computer performs calculations (may be, infinitely) and sometimes produces the results (to output). It also may be unloaded by another service unloader.
The external behaviour of module Procedure is relatively simple, so it can be replaced by a single node.
We tried to identify the distinctive features of AR-nets, that would possibly allow them to be a successful base of some modular (and/or hierarchical) formalism. We also performed some simple analyses of expressiveness of specific modular constructs and decidability of basic module equivalences. It is also shown that modular AR-nets may be a convenient modeling tool.
Since AR-nets are expressively equivalent to general Petri nets, all the results, mentioned in the paper, can be applied to a standard Petri net syntax (in terms of places and transitions). However, in contrast to ordinary Petri nets, the set of nodes is homogeneous here and hence the syntax of module seems quite compact and natural.
We also believe that our work shows the opportunities provided by “coloured” arcs in Petri nets. Two-coloured arcs allowed us to remove the partition of nodes into places and transitions. Obviously, the process of generalization can go further, to a more complex/useful arcs/relations.
The possible directions of a future research in the area of modular AR-nets are: the decidability of certain equivalences of modules; the problem of finding the most effective (smallest/the least connected) decomposition of a given net; the refinement of nodes; the algebraic manipulations with AR-nets and modules; the synchronous compositions (requires additional constructs); etc. Proceedings of CompoNet and SUMo 2011 48