A class of hypernets with token creation and decidable reachability problem Marek A Bednarczyk1 ,2 , Piotr Jóźwiak3, and Wiesław Pawłowski1,3 1 IPI PAN, Gdańsk, Poland 2 ZWI PJWSTK, Gdańsk, Poland 3 II UG, Gdańsk, Poland Abstract. The formalism of Petri hypernets is extended by allowing creation of unstruc- tured 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. 1 Introduction 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 [8] the first condition is implemented as follows. A variable vx,y is associated to every arrow between nodes x and y in the net. Then, a transition t is enabled in a marking M only when there is a map ζ which associates objects to variables so that from each input place p of t the map choses object ζ(vs,t ) in M . Suppose then that the same variable labels arrows from two or more input places of t. Then the transition may fire only if there are references to the same object in all these places. Thus, such object nets operate on the simple type of abstract references with equality. 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 [10, 11]. On the other hand Petri hypernets, see [2], do not admit such testing for equality. An instructive way to compare the formalism proposed by Kummer with hypernets is to say that in hypernets each transition has an injective labeling of input and output arrows. In hypernets this is done by representing an object net as a synchronous product of state machine nets. Consequently, one cannot use such equality tests as described above. This gives hope that an extension which allows creation might not yield a framework with undecidable reachability problem. We introduce coloured Petri hypernets, abbr.: cPH, as an extension of Petri hypernets. This is done by admiting private transitions in agents which, when fire, create unstructured tokens. 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ôle of colours. This seems a right thing to do in order to maintain finitary character of the formalism. Besides, in [8] the reduction goes via reference to the reachability of the empty marking. In an earlier paper [1] it has been shown that each marked hypernet can be translated to a 1-safe net system with an isomorphic case graph. Here we extend this construction and define a translation that maps a marked cPH to a P/T net system in such a way that their state spaces are isomorphic. This reduces the reachability problem for coloured Petri hypernets to that of P/T nets. Whence the reachability problem for coloured Petri hypernets is also decidable. 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. Sec- tion 3 introduces the formalism of coloured Petri hypernets. Section 4 provides the translation and presents the main result of the paper. 2 Petri hypernets Our idea is to modify the definition of Petri hypernets given in [1] as little as possible so that creation of agents is allowed. First, we explain the static structure, and then the dynamic behaviour of hypernets. 2.1 The static structure of Petri hypernets Let us start by recalling some terminology and definitions from [1]. A hypernet is a finite set of agents. A (mobile) agent is a synchronous product of a finite set of modules. A module is a state- machine net. Thus, in an agent each transition has the same number of pre- and post-conditions. 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, [13, 7], the only novelty so far is the requirement that our agents are explicitly decom- posed into synchronous products of their sequential components. Note that by [5] any elementary net admits such a decomposition, and the same holds for 1-safe Petri nets, see [3]. 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. FAα (?β, t) implies α 6= β ∧ FAβ (p, t) for some p ∈ PAβ , (1) FAα (t, !β) implies α 6= β ∧ FAβ (p, t) ∧ FAβ (t, q) for some p, q ∈ PAβ . (2) Above PAα , TAα and FAα , denoteSthe respective components of S an α-module of A. In the sequel we let PA = b b {TAα | α ∈ Σ } denote the sets of local {PAα | α ∈ Σ } and TA = 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ôles 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, !). Conversly, an agent of sort β can perform t with FAα (t, !) only together with its super-agent, and 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 FAα (t, !β) and its sub-agent in its β-module which intends to perform t with FAα (?, t). This idea is 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 α: t β: t p Fig. 1. Structural consistency between modules of an agent. with its tokens, i.e., sub-agents. Assume that α-module of an agent contains transition t with flow FAα (?β, t), i.e., t intends to get an α-agent from within its sub-agent stored in β-module. Then 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. We use a convention to draw FAα (?β, t) and FAα (t, !β) as links between the occurrence of t in 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. Given agent A and any t ∈ TAα let preαA (t) and postαA (t) denote the (necessarily unique) pre- 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 [1] Suppose one wants to model an airport as an agent in which two types of agents are to be handled: travellers and planes. A suitable hypernet should thus contain at least three sorts: let π be the sort for planes, τ for passengers and α for airports. 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. A τ: hall deplane board π: lg bg land refuel take-off Fig. 2. Structure of an airport agent. 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 super- agent 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. S that the agents in N have mutually disjoint sets of local places. Thus, any place It is assumed p ∈ PN = b {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. [2]. Definition 4. The state of a hypernet, called hypermarking, is a sort-preserving partial function µ : N ⇀ PN . 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. Let us concentrate now on a single α-module of A such that t ∈ TAα . If the input and output 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. S – t ∈ TN = b {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 }. A' A α: α: β: β: t t A A' t (1) t (2) α: α: Fig. 3. Two instances of inter-level communication flow A α A′ from A to A′ . Flow up on the left, flow down on the right S α b PN ∩ S – In(Γ ) = α∈Σ {pre A (t) | A ∈ T } is the set of local inputs of Γ . – Out(Γ ) = b PN ∩ α∈Σ {postαA (t) | A ∈ T } is the set of local outputs of Γ . – ξ : In(Γ ) → N is token choice function of Γ . ξ is injective and sort preserving: σ(ξ(p)) = σ(p) for each place p ∈ In(Γ ). – Tξ = {ξ(p) | p ∈ In(Γ ) } is the set of passive agents or tokens of Γ . Note that an agent can be active and passive at the same time. – ↑ : Tξ → T yields super-agents for each token of Γ . Formally, A′ ↑= A iff ξ(p) = A′ for some p ∈ PA . 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) α A, where p = preβA (t) β 5. A ∈ T and FAα (t, !β) implies S ξ(p) ∈ T and A α ξ(p), where p = pre A (t) 6. The undirected graph (T , α∈Σ α ) is connected. 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 on- board. 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 A T1 T2 hall P1 P2 deplane board c1 c2 board deplane lg bg board deplane land refuel take-off Fig. 4. Inter-level agent communication flow: P1 τ A and A τ P2. 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. Intuitively, agents in T move those in Tξ . The initial locations of token agents Tξ is given by ξ −1 . 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) = b preαA1 (t) and postα (c) = b postαAn (t). 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 corre- sponding 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 ⇀ PN 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.  trgΓ (µA) A ∈ Tξ µ′ A = µA A∈/ Tξ 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 A T1 T2 hall P1 P2 deplane board c1 c2 board deplane lg bg board deplane land refuel take-off Fig. 5. T2 is boarding plane P2 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 [9]. 3 Petri hypernets with creation of coloured tokens Extension of a formalism in which individual agents may contain other agent rises basic yet im- portant 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 inves- tigate 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 inter- action 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 pre- condition 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. 3.2 Coloured tokens and hypermarkings 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 ⇀ PN 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ôle 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 ⇀ PN 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.  ′ trgΓ (µA) A ∈ Tξ µA= µA A∈ / Tξ   ν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. 3.4 Coloured hypernets—an example Fig. 6 shows a variant of Airport hypernet in which two travellers agents with empty structure have been replaced by tokens. The coloured hypernet contains also a transition nT capable of creating A nT hall P1 P2 deplane board c1 c2 board deplane lg bg board deplane land refuel take-off Fig. 6. A coloured version of Airport from Fig. 4 agents. The effect of firing nT twice in a row from the given state is shown on Fig. 7. A nT hall P1 P2 deplane board c1 c2 board deplane lg bg board deplane land refuel take-off Fig. 7. Coloured token creation in Airport from Fig. 6 4 From coloured Petri hypernets to P/T nets In this section we show that the semantics of coloured Petri hypernets can be explained by means of finite P/T nets, cf. [12]. The construction is done in two stages. 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 ∪ S BH where CH =b {hpi | p ∈ {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 [1] consortia become transitions of the resulting net. Each consortium contains detailed information about the rôle of its active and passive agents, including the rôle of passive indistinguishable agents. This, on the basis of Prop. 3 and Def. 11, is reflected in the definition of flow of NH above. The effect of structural expansion of coloured hypernet from Fig. 6 gives rise to the marking depicted on Fig. 8. nT deplane board board deplane refuel refuel Fig. 8. Structural expansion of hypernet from Fig. 6 4.2 From marked coloured Petri hypernets to P/T net systems Let (µ, ν) be a coloured hypermarking on H. Define marking M(µ,ν) : P → N of the corresponding Petri net PH as follows.  1 µA = p M(µ,ν) hp, Ai = (3) 0 µA 6= p M(µ,ν) hpi = νp (4) 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 (5) 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 (6) νM p = M hpi (7) 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. 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 . Moreover, M [Γ iM ′ in NH and M satisfies (5) then M ′ satisfies (5) as well. So the result follows since (µ, ν)[Γ i(µ′ , ν ′ ) in H implies M(µ,ν) [Γ iM(µ′ ,ν ′ ) in NH holds by 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. nT deplane board board deplane refuel refuel Fig. 9. Expanded marked hypernet from Fig. 7 5 Conclusions and future work Petri hypernets were introduced inside the nets-within-nets paradigm in [2] as a visual framework suitable for modeling mobility of agents. The main difference with other approaches to mobility based on Petri nets is that in hypernets the hierarchy of agents may evolve. 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 [4]. In [1] the authors explained Petri hypernets by means of a translation into 1-safe Petri nets. This translation not only shows that hypernets are well rooted inside the theory of Petri nets. Besides this foundational aspect, the translation allows us to apply the rich set of techniques and algorithms developed over the years for analyzing 1-safe nets (see, for example, [6, 12]). Among them, we find algorithms to check liveness, reachability of a place or of a marking, fairness properties, and so on. The family of methods based on the computation of place- and transition-invariants can then be applied in order, for instance, to check safety properties of a hypernet. 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/de- struction 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 [4] to hypernets with agent creation. Formalisms based on the nets-within-nets paradigm often fall victims of undecidability of fun- damental problems, like reachability. We plan to compare our approach with some of them, e.g., [7], to better understand the reasons. References 1. Marek A. Bednarczyk, Luca Bernardinello, Wiesław Pawłowski, and Lucia Pomello. From Petri hy- pernets to 1-safe nets. In Daniel Moldt, editor, Proceedings of the 4th International Workshop on Modelling of Objects, Components, and Agents, MOCA’06, volume Bericht 272, FBI-HH-B-272/06, pages 23–43. Department für Informatik, Universität Hamburg, 2006. 2. Marek A. Bednarczyk, Luca Bernardinello, Wiesław Pawłowski, and Lucia Pomello. Modelling mobility with Petri hypernets. In José Luiz Fiadeiro, Peter D. Mosses, and Fernando Orejas, editors, Recent Trends in Algebraic Development Techniques. 17th International Workshop WADT 2004, Barcelona, Spain, March 27-30, 2004. Revised Selected Papers, volume 3423 of LNCS, pages 28–44. Springer- Verlag, 2005. 3. Marek A. Bednarczyk and Andrzej M. Borzyszkowski. On concurrent realization of reactive systems and their morphisms. In Hartmut Ehrig, Gabriel Juhás, Julia Padberg, and Grzegorz Rozenberg, edi- tors, Unifying Petri Nets, volume 2128 of Lecture Notes in Computer Science, pages 346–379. Springer, 2001. 4. Marek A. Bednarczyk, Wojciech Jamroga, and Wiesław Pawłowski. Expressing and verifying temporal and structural properties of mobile agents. In Ludwik Czaja, editor, Proceedings of the Concurrency, Specification and Programming Workshop CS&P’05, pages 57–68, 2005. 5. Luca Bernardinello. Synthesis of net systems. In Marco Ajmone Marsan, editor, Application and Theory of Petri Nets, volume 691 of Lecture Notes in Computer Science, pages 89–105. Springer, 1993. 6. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In Reisig and Rozenberg [12], pages 374–428. 7. Michael Köhler and Heiko Rölke. Properties of object Petri nets. In Wil van der Aalst and Eike Best, editors, Applications and Theory of Petri Nets 2004, Proceedings, volume 3099 of LNCS, pages 278–297. Springer-Verlag, 2004. 8. Olaf Kummer. Undecidability in object-oriented Petri nets. Petri Net Newsletter, 59:18–23, 2000. 9. Olaf Kummer, Frank Wienberg, Michael Duvigneau, Jörn Schumacher, Michael Köhler, Daniel Moldt, Heiko Rölke, and Rüdiger Valk. An extensible editor and simulation engine for petri nets: Renew. In Jordi Cortadella and Wolfgang Reisig, editors, ICATPN, volume 3099 of Lecture Notes in Computer Science, pages 484–493. Springer, 2004. 10. Irina A. Lomazova. Nested petri nets — a formalism for specification of multi-agent distributed systems. Fundamenta Informaticae, 43((1-4)):195–214, 2000. 11. Irina A. Lomazova and Philippe Schnoebelen. Some decidability results for nested petri nets. Lecture Notes in Computer Science, 1755:208–220, 2000. 12. Wolfgang Reisig and Grzegorz Rozenberg, editors. Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, volume 1491 of LNCS. Springer, 1998. 13. Rüdiger Valk. On processes of object Petri nets. Technical Report FB-185, Fachbereich Informatik, Universität Hamburg, 1996.