The formalism of Petri hypernets is extended by allowing creation of unstructured tokens. Any two such tokens are then declared indistinguishable, unless they have different sorts, i.e., colours. Under this assumption it is possible to provide a construction that to each coloured Petri hypernet associates a P/T net with an isomorphic case graph. Hence, the reachability problem for coloured Petri hypernets is decidable. Let us consider a high level Petri net formalism in which the nets manipulate tokens which are references to some objects. Following [8] let us assume that the following conditions are satisfied. 1. Within the formalism the “references to objects can be checked for identity”. 2. The net should create fresh objects whenever creation takes place.
Kummer shows that under these assumptions the problem of reachability of the empty marking reduces to the problem of reachability of 2-counter automata, and thus it is undecidable.
In formalism introduced in [
It turns out that undecidability of reachability problem holds for many non-trivial variants of
higher order nets, and for nets-within-nets approaches in particular. This includes many classes of
object nets studied in Hamburg, and nested Petri nets introduiced by Lomazova, see [
On the other hand Petri hypernets, see [
It is assumed that tokens created in this way are distinguishable only if they have different
sorts—each agent in a hypernet has a sort assigned to it. Thus, the sorts play the rˆole of colours.
This seems a right thing to do in order to maintain finitary character of the formalism. Besides, in
[
In an earlier paper [
In what follows standard notational conventions regarding Petri nets and elementary set theory are used. For instance, |A| denotes the cardinality of a set A, a singleton set is identified with its content.
The paper is organised as follows. Section 2 recalls the formalism of Petri hypernets. Section 3 introduces the formalism of coloured Petri hypernets. Section 4 provides the translation and presents the main result of the paper. 2
Our idea is to modify the definition of Petri hypernets given in [
The static structure of Petri hypernets
Let us start by recalling some terminology and definitions from [
The state of a hypernet, called hypermarking, is given as a distribution of agents among places
(also called locations) of other agents. Thus, in comparison with the classical nets-within-nets
approaches, [
Another restriction imposed on hypernets is that each agent and each module has assigned a sort. Let Σ be a finite set of sorts, and let α, β, . . . range over Σ. We require that an agent of a sort α can be hosted only by the places of modules of sort α.
An extension of the classical idea comes with the notion of communication ports. Formally, let I = {?} ∪ {?β | β ∈ Σ } and O = {!} ∪ {!β | β ∈ Σ } be the sets of input and output ports, respectively. The purpose of ports is to allow for the exchange of tokens, i.e. agents, between agents. This allows the hierarchy of agents to evolve, unlike in some other approaches based on nets-within-nets paradigm.
Definition 1. A module of sort α (α-module) is a, possibly empty, finite Petri net N = (P, T , F ), where P is the set of local places, T is the set of transitions, and F ⊆ ((P ∪ I) × T ) ∪ (T × (P ∪ O)) is the flow relation. We assume that P ∩ (I ∪ O) = ∅ and |pre (t)| = 1 = |post (t)| for all t ∈ T . The last condition above says that each transition has exactly one pre- and one post-condition, either a local place, or a communication port. This condition is relaxed in the sequel to allow creation of agents.
Definition 2. An agent A = {NAα | α ∈ Σ } is a Σ-indexed set of modules, We call NAα the αmodule of A, and assume PAα ∩ PAκ = ∅ whenever α 6= κ.
Modules should satisfy the following structural consistency conditions.
α 6= β ∧ FAβ (p, t) for some p ∈ PAβ, α 6= β ∧ FAβ (p, t) ∧ FAβ (t, q) for some p, q ∈ PAβ . (1) (2) Above PAα, TAα and FAα, denote the respective components of an α-module of A.
In the sequel we let PA =b S {PAα | α ∈ Σ } and TA =b S {TAα | α ∈ Σ } denote the sets of local places and transitions of A, respectively.
Different modules do not share locations, but they can share transitions. Shared transition are used for the synchronisation of the respective modules. When each module of an agent is the empty net, then the agent behaves like an unstructured token. This observation will serve as the basis for identification of such unstructured tokens later on.
Ports ? and ! serve to communicate with agent’s current super-agent. Ports of the form ?β and !β serve to communicate with agent’s sub-agents located in its β-module. In the sequel the two kinds of ports serve rˆoles complementary to each other. Let us consider first moving a token agent up in the hierarchy. Then, for instance, an agent can perform action t with FAα(?β, t) only together with one of its sub-agents in its β-module, and provided the sub-agent can perform t with FAα(t, !).
provided its super-agent can perform t with FAα(?β, t). Similar cooperation must take place when moving tokens down the hierarchy, e.g., between an agent which wants to perform action t with
formally captured in the sequel by the notion of consortium.
To cope with graphical representation of ports the classical notation is somewhat extended. Consider the meaning of Def. 2(1) visualised on Fig. 1. It deals with communication of an agent α: β: p t t with its tokens, i.e., sub-agents. Assume that α-module of an agent contains transition t with flow
Def. 2(1) asserts that β must be different from α, and that the β-module must contain transition t, and the precondition of t in the β-module must not be a port.
Thus, the consistency of a request by α-module to receive something from within agents in the β-module can be locally verified by looking at the agents in the local place p such that FAβ (p, t). Condition Def. 2(2) states that when agent wants to send something down, then t must be present in the β-module. Moreover, pre- and post-condition of t in β module must be locations, not ports.
the α-module and the input and output arcs of t in the β-module. Intended communication with super-agents is graphically represented by broken line half-circles, see Fig. 2.
and post-condition of t in the α-module of A, respectively. Note that preαA(t) and postαA(t) can be either local places or communication ports.
Airport example, see [
Fig. 2 describes a possible structure of an airport agent which consists of two non empty modules: π-module for plane handling, and τ -module for travelers.
τ: π: land
A
hall
The π-module captures the usual plane handling procedure: plane lands from above; disposes of its passengers (if any); refuels; boards new passengers and finally takes off. Some of these activities are captured by transitions like land and take-off which use communication with the implicit superagent of the airport agent to move plane agents into and out of the airport. Transition refuel , which moves plane agents between locations of the airport agent does not require any synchronisation. Finally, transitions deplane and board are present in both modules and their firing does require synchronisation. Intuitively, to fire board, say, we need a traveler agent in location hall and a plane agent in location bg . Moreover, the transition in the τ -module has an output port as the postcondition, so the plane agent should be prepared to engage in board with flow F (?, board ). Definition 3. A Petri hypernet is a finite family N of agents together with sorting, i.e., a function σ : N → Σ that assigns to each agent its sort.
It is assumed that the agents in N have mutually disjoint sets of local places. Thus, any place p ∈ PN =b S {PA | A ∈ N } can be assigned its sort σ(p) = α where α is the sort of a module of the (unique) A ∈ N , such that p ∈ PAα.
In hypernets the locations of an agent are distributed among its modules. Hence, the state of
a hypernet is uniquely defined as a many-to-one correspondence between agents and locations,
cf. [
Definition 4. The state of a hypernet, called hypermarking, is a sort-preserving partial function μ : N ⇀ P N . 2.2
The dynamics of Petri hypernets The dynamics of hypernet reflects their ability to change state of the system.
Suppose t ∈ TA is a transition of agent A. Then A in a given state can perform t only if all its αmodules such that t ∈ TAα can perform t. This means that we assume inter-module synchronisation on common transitions.
places of t in the module are locations, i.e., local places, then in order to perform t it is enough to find a token in preαA(t) and move it to postαA(t). Otherwise, either preαA(t) or postαA(t), or both, are communication ports. Then inter-level synchronisation between agents should take place. Flow of tokens and consortia.
The inter-module synchronisation is static in the sense that it concernes a fixed set of modules of an agent. The inter-agent interaction is dynamic—it depends on the current hypermarking— distribution of agents among locations. Our aim is to explain how such a distribution may evolve.
Consider agents A and A′ which try to help each other to perform transition t by establishing a communication link for α-tokens flow from A to A′ , notation A α A′ . Such flow can go either up or down the hierarchy. The first case is described on the left, the second on the right of Fig. 3. The existence of an α-flow requires that two conditions hold.
Adjacency: One of the agents should be the super-agent of the other.
Matching: Each agent should match the communication request of the other. Airport example (cntd.) In Fig. 4 the airport agent contains two plane agents P1 and P2, and also two traveller agents T1 and T2. It should be clear that P1 τ A and A τ P2 hold.
Fig. 4 also demonstrates that in hypernets inter-module and inter-agent synchronisation may take place at the same time. Thus, one is interested not just in pairs of agents, but in groups of agents which should cooperate with each other to ensure that together all their synchronisation and communication requests related to execution of a shared transition are satisfied.
Let N be a hypernet with sorting σ and consider a triple Γ = (t, T , ξ) which satisfies the following.
– t ∈ TN =b S {TA | A ∈ N } is a transition of N . – T ⊆ N is the set of active agents of Γ .
All active agents share t, i.e., T ⊆ {A ∈ N | t ∈ TA }.
α: t
Definition 5. Consider Γ as above and active agents A, A′ ∈ T . Then, there is an α-flow from A to A′ in Γ , written A α A′ , if one of the following conditions is satisfied. flow up postαA(t) = ! and ξ(preβA′ (t)) = A and preαA′ (t) = ?β and β = σ(A). flow down postαA(t) = !β and ξ(preβA(t)) = A′ and preαA′ (t) = ? and β = σ(A′ ).
Finally, we are ready to define the notion of consortium.
Definition 6. A triple Γ as above is a consortium provided the following hold. 1. T is non-empty. 2. A ∈ T and FAα(?, t) implies A ∈ Tξ and A↑ α A 3. A ∈ T and FAα(t, !) implies A ∈ Tξ and A α A↑ 4. A ∈ T and FAα(?β, t) implies ξ(p) ∈ T and ξ(p) 5. A ∈ T and FAα(t, !β) implies ξ(p) ∈ T and A 6. The undirected graph (T , Sα∈Σ α) is connected.
α A, where p = preβA(t) α ξ(p), where p = preβA(t) Most of the conditions have a simple justification. Condition 1 says that at least one active agent has to be involved. Conditions 2-5 stipulate that members of T provide matching communication capabilities for other members of the group. Note that structural consistency conditions of Def. 2 guarantee the existence of a suitable location p. Finally, condition 6 says that T is a minimal such group of agents.
Note that transaction may involve just one active agent, see for instance transition refuel in our running example.
Airport example (cntd.). Let us consider airport agent from Fig. 2 together with two airplane agents P1 and P2, and two traveller agents T1 and T2. The plane agents have a very simple structure. It consists of just one non empty module for traveller handling. A plane is always ready to accept a new passenger from its super-agent, and always ready to dispose of any travellers onboard. Traveller agents are unstructured tokens.
The group together with two consortia is depicted on Fig. 4. One consortium involves deplane and agents A and P1 as active agents. The local input places of these agents are lg and c1 . The T2 P2
hall board land board passive token agents chosen for these places are P1 and T1, respectively. Note that P1 is both active and passive. This means that it will move a token, here T1, and be moved as a token at the same time. There is one flow involved in this consortium, namely P1 τ A.
Another consortium involves board and agents A and P2 as active agents. The local input places of these agents are bg and l . The passive token agents chosen for these places are P2 and T2, respectively. The only flow involved is A τ P2.
Chains of flow.
A consortium Γ = (t, T , ξ) is a minimal group of vertically interconnected agents which together can change the state of the hypernet by moving some agents from one location to another. To formalise this idea we need to know which agents to move, and also their initial and final locations.
So, the only problem is to find their final destination. The ability to find such unique locations stems from conditions 2-5 of Definition 6. The mechanism involved is explained by means of a generalisation of the notion of α-flow among the members of consortium Γ .
Definition 7. An α-chain of flow in consortium Γ is a finite non-empty sequence c = A1 . . . An of agents from T , such that Ai α Ai+1 for 1 ≤ i < n.
Let preα(c) = preαA1 (t) and postα(c) = postαAn (t).
b b Proposition 1. Let Γ = (t, T , ξ) be a consortium. For any agent A ∈ T such that preαA(t) is a location there exists a unique α-chain c = A1 . . . An such that A = A1 and postαAn (t) is a local place as well.
Given an output place of Γ one can start building a chain of flow which will lead to a corresponding input location.
Proposition 2. Each consortium Γ = (t, T , ξ) induces a sort-preserving bijection trgΓ : In(Γ ) → Out(Γ ) where trgΓ (p) = q iff there is a κ-chain of flow c in Γ , where κ = σ(p), such that p = preκ(c) and q = postκ(c). Moreover, for p ∈ In(Γ ) if trgΓ (p) ∈ In(Γ ) then trgΓ (p) = p. Proof. The first part follows immediately by Proposition 1. So, assume q = trgΓ (p) ∈ InΓ () for some p ∈ In(Γ ). Then, by definition of trgΓ it follows that q = postαA(t) for the last agent A ∈ T in any α-chain of flow that starts with p.. But from q = trgΓ (p) ∈ In(Γ ) it follows that q = preαA(t). So, this chain contains just A, and so p = q follows. 2 A consortium is enabled at a hypermarking when the choice of the passive tokens in consortium agrees with their location described by the hypermarking. The effect of firing enabled transition is to update the hypermarking by synchronously moving the passive agents to locations prescribed by trg function.
Definition 8. Let μ : N ⇀ P N be a hypermarking of N . Then consortium Γ = (t, T , ξ) is enabled at μ, notation μ[Γ i, if μ(ξ(p)) = p for all p ∈ In(Γ ). Γ enabled at μ can fire, yielding a new hypermarking μ′ defined as follows. Consider a hypernet (N , σ) with an initial hypermarking μ. Then its case graph has hypermarkings reachable from μ as states and firings of consortia as transitions.
Boarding a passenger—an example of hierarchy change
The example below demonstrates the effect of an inter-level communication between agents. A situation at the airport as described on Fig. 4, offers two possible consortia—corresponding to T2 P2 T1 P1
hall board bg board c1 deplane land take-off board c2 the deplane and board actions respectively. The latter consists of a plane P2 and the airport A as active agents and a traveller T2 and plane P2 as passive tokens. As a result of firing the consortium the passenger T2 is moved from the passenger’s lounge (place hall) to the plane and vanishes from the level of the airport. Plane P2 stays in place bg. The new situation is depicted on Fig. 5.
Note that such a change is not supported by most theories that deal with nets-within-nets
formalisms. On the other hand hierarchy change can be modelled in Renew, see [
Extension of a formalism in which individual agents may contain other agent rises basic yet important questions. Let us start by reviewing some of them.
– Can the agents created be complex? Only unstructured/empty agents can be created. – Do we allow destruction of agents? Destruction is not allowed. Thus, we do not have to investigate what happens to an agent which is destroyed or to it’s subagents. – How to cope with unbounded name spaces when creation is allowed? Newly created agents of the same kind (sort) are indistinguishable.
Additionally, to simplify matters it is assumed that creation is local to an agent, i.e., agent interaction does not involve creation. 3.1
Static structure of coloured hypernets Let us start by relaxing the Def. 1 by allowing transitions in a module to have at most one precondition and exactly one post-condition (to allow creation of tokens). The notion of agent given in Def. 2 remains unchanged. The definition of hypernet is modified as follows. Definition 9. A coloured Petri hypernet is a finite family N of agents together with sorting, i.e., a function σ : N → Σ that assigns to each agent its sort. Given α, for any t ∈ TN if preαA(t) = ∅ for some A ∈ N then t ∈ TA′ with A′ ∈ N implies A = A′ . Moreover, for any β ∈ Σ the post-condition postβA(t) is a location, and and if preβA(t) exists then preβA(t) is a location as well. Thus, the restriction imposed on hypernets is that if a transition of an agent lacks a pre-condition in one of its modules then this is a private transition of that agent. Moreover, such transition has only locations as pre- and post-conditions. This assumption has important consequences. Now every consortium related to agent creating transition consists of a singleton active agent. In hypernets every agent has a sort assigned to it. We have postulated that agents which are created are unstructured, so let us refer to any such agent by means of its sort. This also allows to capture the postulate that created agents are indistinguishable: three such agents of sort σ will be represented as 3 · σ.
As a consequence of the above decision one has to modify the notion of hypermarking to allow both: distinguishable and indistinguishable agents in locations.
Definition 10. The state of a coloured hypernet, called hypermarking, consists of a sort-preserving partial function μ : N ⇀ P N and a function ν : PN → N.
Thus, the old notion is extended by another component that simply counts how many unstructured tokens are stored in each location. 3.3
Coloured tokens and consortia Since created agents are unstructured they cannot play the rˆole of active agents. Thus, the notion of consortium for coloured hypernets is almost identical to the basic notion introduced in Def. 6.
The only difference is that now we require that the token choice function ξ for the triple Γ = (t, T , ξ) is partial. The idea here is that if ξ(p) is undefined for some p ∈ In(Γ ) then implicitly an unstructured agent is chosen.
Note also, that the idea of communication flow between agents involves only structured agents. Hence, the definition of flow in Γ , Def. 5, and the definition of consortium, Def. 6, stays the same. The same remark applies to the notion of chain of flow, cf. Def. 7.
Whence, Prop. 1 holds without change, whereas Prop. 2 in case of coloured Petri hypernets needs minute modification.
Proposition 3. Each consortium Γ = (t, T , ξ) induces a sort-preserving injection trgΓ : In(Γ ) → Out(Γ ) where trgΓ (p) = q iff there is a κ-chain of flow c in Γ , where κ = σ(p), such that p = preκ(c) and q = postκ(c). Moreover, for p ∈ In(Γ ) if trgΓ (p) ∈ In(Γ ) then trgΓ (p) = p. Proof. The same arguments as in the proof of Prop. 2. 2 The only difference between the above and Prop. 2 is that now we cannot claim that trgΓ is a bijection, since in the presence of agent creating transitions the caridnality of In(Γ ) could be smaller than that of Out(Γ ). Thus, a simple modification allows to define the dynamics of coloured Petri hypernets as follows.
Definition 11. Let (μ, ν) be a hypermarking of cPH N with μ : N ⇀ P N and ν : PN → N. Consider consortium Γ = (t, T , ξ). Then Γ is enabled at (μ, ν), notation (μ, ν)[Γ i, if for all p ∈ In(Γ ) either μ(ξ(p)) = p when ξ(p)-defined, or ν(p) > 0 when ξ(p)-undefined. Γ enabled at (μ, ν) can fire, yielding a new hypermarking (μ′ , ν′ ) defined as follows. νq + 1 q ∈ Out(Γ ) \ In(Γ ) \ trgΓ ({p ∈ In(Γ ) | ξ(p)-defined }) ν′ q = νq − 1 q ∈ In(Γ ) \ Out(Γ ) ∧ ξ(q)-undefined
νq otherwise The correctness of the above definition stems from Prop. 2. board board c2 agents. The effect of firing nT twice in a row from the given state is shown on Fig. 7.
P1 P1 land land deplane lg deplane lg refuel
hall A A refuel hall board
bg board
bg board c1 deplane board c2 deplane
In this section we show that the semantics of coloured Petri hypernets can be explained by means
of finite P/T nets, cf. [
First, to each coloured hypernet H = (N , σ) we associate an unmarked Petri net NH . Second, to each hypermarking (μ, ν) of H we associate a marking M(μ,ν) of NH in such a way that the dynamic evolution of H from (μ, ν) is isomorphic to the dynamic evolution of NH with M(μ,ν) as an initial marking. 4.1
Structural expansion of coloured Petri hypernets Let H = (N , σ) be a coloured hypernet. Define NH = (P, T , F ) as follows.
Places P = CH ∪ BH where
CH =b {hpi | p ∈ S {PA | A ∈ N } }, BH =b {hp, Ai | σ(p) = σ(A), A ∈ N , p ∈ PN }.
We assume that CH ∩ BH = ∅.
The intended meaning: – Place hp, Ai is used to mark presence of agent A at p in H.
– Place hpi is used to count the number of indistinguishable agents at p in H. Transitions T =b {Γ | Γ is a consortium of H }.
Flow relation F ⊆ P × T ∪ T × P defined as follows.
Let Γ = (t, T , ξ) be a consortium in H. Then F (hp, Ai, Γ ) iff p ∈ In(Γ ) and ξ(p) = A F (Γ, hp, Ai) iff p ∈ Out(Γ ) and ξ(trgΓ−1(p)) = A.
F (hpi, Γ ) iff p ∈ In(Γ ) and ξ(p)-undefined
F (Γ, hpi) iff p ∈ Out(Γ ) \ trgΓ (In(Γ )) or ξ(trgΓ−1(p))-undefined.
Thus, each location p of H is modeled in NH by a number of copies. First, there is hp, Ai for each agent A of an appropriate sort. Secondly, there is hpi to cope with the indistinguishable agents that can be stored in p.
Just as in [
The effect of structural expansion of coloured hypernet from Fig. 6 gives rise to the marking depicted on Fig. 8.
deplane board <hall>
<c1> board deplane refuel
refuel <bg,P2>
Petri net PH as follows.
M(μ,ν)hp, Ai =
M(μ,ν)hpi = νp 1 μA = p 0 μA 6= p
It is not true that every marking on NH can be obtained from a hypermarking by the above construction. For instance, markings of the form M(μ,ν) satisfy.
M hp, Ai ≤ 1 and (∀p, q ∈ PN ) M hp, Ai = 1 = M hq, Ai ⇒ p = q If, however, a marking of NH satisfies (5) then the converse construction can be given as follows. μM A = p, provided M hp, Ai = 1 νM p = M hpi It should be evident that together the constructions define a bijection between hypermarkings of coloured Petri hypernet H and markings of NH that satisfy (5). From this observation the main result follows easily. (3) (4) (5) (6) (7) Theorem 1. The hyper-case graph of a marked coloured hypernet is isomorphic to the case graph of the corresponding Petri net system.
Proof. Let H be a coloured Petri hypernet with hypermarking (μ, ν).
Then (μ, ν)[Γ i in H iff M(μ,ν)[Γ i in NH .
construction for an arbitrary consortium Γ of H. 2
On the basis of the above one can easily reduce the problem of reachability of a hypermarking from a given one to the problem of reachability in the world of P/T net systems. Since the latter is decidable, it follows that so is the former.
Corollary 1. The reachability problem for coloured Petri hypernets is decidable. Clearly, the corollary has philospohical rather than practical impact since the complexity of the decidability procedure is very high. Additionally, the process of expansion could blow up the size of the hypernet.
The marked coloured hypernet from Fig. 7 gives rise to the marking depicted on Fig. 9 in the expanded version.
deplane board <hall>
<c1> board deplane refuel
refuel
Petri hypernets were introduced inside the nets-within-nets paradigm in [
The individual agent semantics of hypernets (each agent is identifiable) is another difference
between hypernets and other models. The choice of this semantics leads to a logic in which the
dynamic and structural properties of agents can be expressed and model checked as proposed in [
In [
In this note an extension of Petri hypernets was introduced which allows creation of agents with empty structure. To bound the name space of the objects in the formalism we have imposed restriction that any two such agents of the same kind (sort) are not distinguishable.
With this assumption it was possible to provide a translation of the extended class of hypernets to P/T nets. Again, the translation establishes an isomorphism between states of a hypernet and a class of reachable markings of the corresponding P/T net. Thus, again, one can apply the theory developed to study P/T nets to cope with this class of hypernets.
Concerning future work—it seems that there should be no problem to allow
consumption/destruction of agents together with creation. It seems, however, that this may be done in several ways.
Here, the question to answer is: What happens to sub-agents of an agent if the latter is destroyed?
We plan also to investigate extensions of logic developed in [
Formalisms based on the nets-within-nets paradigm often fall victims of undecidability of
fundamental problems, like reachability. We plan to compare our approach with some of them, e.g., [