Functorial Analysis of Algebraic Higher-Order Net Systems with Applications to Mobile Ad-Hoc NetworksThis work has been partly funded by the research project eserved@d = *@let@token 2551forMANET (see ` `%%%`#`&12_`__~~~) of the German Research Council. Electronic Communications of the EASST Volume 40 (2011) Proceedings of the 4th International Workshop on Petri Nets and Graph Transformation (PNGT 2010) Functorial Analysis of Algebraic Higher-Order Net Systems with Applications to Mobile Ad-Hoc Networks Ulrike Golas, Kathrin Hoffmann, Hartmut Ehrig, Alexander Rein and Julia Padberg 20 pages Guest Editors: Claudia Ermel, Kathrin Hoffmann Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Functorial Analysis of Algebraic Higher-Order Net Systems with Applications to Mobile Ad-Hoc Networks∗ Ulrike Golas1, Kathrin Hoffmann23, Hartmut Ehrig2, Alexander Rein2 and Julia Padberg3 1 golas@zib.de Konrad-Zuse-Zentrum für Informationstechnik Berlin, Germany 2 hoffmann|ehrig|alex@cs.tu-berlin.de Technische Universität Berlin, Germany 3 padberg@informatik.haw-hamburg.de Hochschule für Angewandte Wissenschaften Hamburg, Germany Abstract: Algebraic higher-order (AHO) net systems are Petri nets with place/ transition systems, i.e. place/transition nets with initial markings, and rules as to- kens. In several applications, however, there is the need for explicit data modeling. The main idea of this paper is to introduce AHO net systems with high-level net systems and corresponding rules as tokens. We relate them to AHO net systems with low-level net systems as tokens and analyze the firing and transformation prop- erties of the corresponding net class transformation defined as functors between the corresponding categories of AHO net systems. All concepts and results are explained with an example in the application area of mobile ad-hoc networks. From an abstract point of view, mobile ad-hoc networks consist of mobile nodes which communicate with each other independent of a stable infrastructure, while the topology of the network constantly changes depending on the current position of the nodes and their availability. To ensure satisfactory team cooperation in workflows of mobile ad-hoc networks we use the modeling technique of AHO net systems. Keywords: algebraic higher-order nets, mobile ad-hoc networks, skeleton functor 1 Introduction and Related Work Place/transition (P/T) systems and their variants are an established process definition language for the representation, validation and verification of workflow procedures (see, e. g., [vdA03] for an overview), where P/T nets represent process schemes and P/T systems describe the behavior of process instances due to their initial markings. The paradigm of nets as tokens has been introduced by Valk [Val98] where so-called object nets are token within another net, called a system net. In elementary object systems, object nets can move through a system net and interact ∗ This work has been partly funded by the research project for MA`NET (see http://tfs.cs.tu-berlin.de/formalnet/) of the German Research Council. 1 / 20 Volume 40 (2011) mailto:golas@zib.de mailto:hoffmann$|$ehrig$|$alex@cs.tu-berlin.de mailto:padberg@informatik.haw-hamburg.de http://tfs.cs.tu-berlin.de/formalnet/ Functorial Analysis of Algebraic Higher-Order Net Systems with both the system net and other object nets. This allows to change the marking of the object nets, but not their net structure. In [HME05, EHP+07], the concept of reconfigurable place/transition net systems has been introduced which is most important to model changes of the net structure while the system is kept running. In detail, a reconfigurable P/T net system consists of a P/T net with marking and a set of rules. In these nets, not only the follower marking can be computed but also the structure can be changed by rule application to obtain a new P/T net system that is more appropriate with respect to some requirements of the environment. For rule-based transformations of P/T net systems we use the framework of net transformations [EEPT06] following the double-pushout (DPO) approach of graph transformation systems and the notation of Petri nets as monoids [MM90]. The basic idea behind net transformations is the stepwise development of P/T net systems by given rules. One may think of these rules as replacement systems where the left-hand side is replaced by the right-hand side while preserving a context. In low-level Petri nets, the tokens are indistinguishable. The integration of Petri nets with data type descriptions has led to high-level nets as powerful specification techniques like alge- braic high-level (AHL) nets [PER95], which can also be transformed within the DPO approach [Pra08]. In [HME05], we have introduced the paradigm nets and rules as tokens by a high-level model with a suitable data type part. The model called algebraic higher-order (AHO) net system exploits some form of control not only on the rule application but also on token firing. An AHO net system is defined by an AHL net system with net places and rule places, where the mark- ing is given by suitable low-level net systems or rules, respectively, on these places. As shown in [BRHM06], this paradigm has been very useful to model applications in the area of mobile ad-hoc networks. Mobile ad-hoc networks (MANETs) consist of mobile nodes forwarding data to other nodes based on the network connectivity independent from a stable infrastructure. The constant change of the network’s topology depends on the current position of the nodes and their availability. A typical example of a complex application is a team communicating using hand-held devices and laptops as in emergency scenarios [PHE+07]. In such a scenario, each team member performs specific activities while different teams collaborate through the interleaving of all the different workflows. Normally, workflows in mobile environments are not fixed once and for all at design time but are constantly adapted at run time predicting disconnections or reorganizing activities. This requires on the one hand a suitable description of the distributed workflows and on the other hand expressive techniques for the adaption. Research on MANETs [AZ03] has focused mainly on the infrastructure at the lower levels of the ISO/OSI-standards. To apply MANETs in larger operations it is necessary to abstract from the network layer. In [RMPM03], an interface for network services that can be used by applications abstracting from the underlying protocols is suggested. In contrast to approaches using models mainly for the network we propose modeling the application in terms of workflows, such that the adaption of workflows to accommodate the requirements in an ad-hoc setting are met. Our experience with the case study in [PEH07] has clearly shown the need to integrate data on the level of workflows. The main idea of this paper is to introduce AHO net systems with high- level net systems and corresponding rules as tokens. We relate them to AHO net systems with low-level net systems and rules as tokens, and analyze the firing and transformation properties of the corresponding net class transformation defined as functor between corresponding categories Proc. PNGT 2010 2 / 20 ECEASST of AHO net systems. This functor is based on the corresponding functor from high-level to low- level nets [Urb03]. All concepts and results are explained with an example in the area of mobile ad-hoc networks. In contrast to [PEH07], where we have used merely low-level net systems, we present now a pipeline emergency scenario where we use data dependent workflows. This paper is organized as follows: In Section 2, we introduce as motivating example a pipeline emergency scenario using data dependent workflows. In Section 3, we define AHO net systems with AHL net systems and rules as tokens as well as their firing behavior and transformations. In Section 4, we present the skeleton functor transforming AHO net systems with high-level tokens to such with low-level tokens and show that enabling and firing is preserved. Finally, in Section 5, we give a conclusion and an outlook to future work. 2 Motivation: Emergency Scenario In emergency scenarios, we can obtain an effective coordination among team members consti- tuting a mobile ad-hoc network through the use of net system and rule tokens. In this way, y less 5 = tt Notify residents of the evacuation persons Assist handicapped the extent possible Guide persons to the immediate area Evacuate homes in p:Tok p’’’:Tok L x x p:Tok p’’’:Tok p’’:Tok p’:Tok R x x x x x x p:Tok p’’’:Tok K rl Request to control traffic into the area Identify the location gas is highest Additional reading the gas indicator Shut off electricity and gas lines gas company Call the Reading the gas indicator Expand the area of evacuation Deny entry Stand by p10:Nat Evacuate homes in the immediate area y y p1:Tok p3:Tok p4:Tok p6:Tok p9:Tok p12:Tok p14:Tok p15:Tok p13:Tok p2:Tok p5:Tok p7:Tok x x x x x x x x x x x x x x x x x x x y x x x p11:Tok x x x y geq 5 = tt Result >= 5% LEL Result < 5% LEL x x p8:Tok x n m : Mor cod(m) = n applicable(rl, m) = tt n tσ : Trans token firing transform(rl, m) net transformation rl rules : Rules (AHON SIG, X ), AHL enabled(n,tσ ) =tt net : Net fire(n,tσ ) AHLNetSys AHLRule Figure 1: Algebraic higher-order net system for emergency scenario 3 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems cooperative work can be adequately modeled by high-level Petri nets with initial markings. The net structure can be adapted to new requirements of the environment during run time by a set of rules, i.e. token firing and net transformation can be interleaved with each other. In contrast to [PEH07], where we have used merely low-level net systems, we present a pipeline emergency scenario based on data dependent workflows. This means that we use AHL net systems and corresponding rules as tokens. In this section, we introduce our emergency scenario and illustrate the main idea of algebraic higher-order (AHO) net systems using high-level net system and rule tokens, while the detailed definitions can be found in Section 3. According to the pipeline emergency scenario1, a natural gas leak of unknown source is detected in a residential area. At the scene, the company officer calls the gas company and requests an additional law enforcement officer to control traffic into the area. Upon the arrival of the gas company, the firefighters evacuate the homes in the immediate area, subsequently deny entry to this area and finally stand by with fully charged hose lines. In fact, the firefighter company as well as the gas company collaborate through the exchange of messages to achieve the common goal. y less 5 = tt Request to control traffic into the area Identify the location gas is highest Additional reading the gas indicator Shut off electricity and gas lines gas company Call the Reading the gas indicator Expand the area of evacuation Deny entry Stand by p10:Nat Evacuate homes in the immediate area y y p1:Tok p3:Tok p8:Tok p4:Tok p6:Tok p9:Tok p12:Tok p14:Tok p15:Tok p13:Tok p2:Tok p5:Tok p7:Tok x x x x x x x x x x x x x x x x x x x y x x x p11:Tok x x x x x x Result < 5% LEL Result >= 5% LEL y geq 5 = tt Figure 2: AHLNetSys′ In Figure 1, the cooperative workflow enacted by the firefighter company is de- picted in the algebraic high-level (AHL) net system AHLNetSys = (AHLNet, M) with AHL net AHLNet and marking M as token on the place net. Such an AHL net system token is called object net system. This object net system is coordinated by an AHO net system at the system level con- sisting of the places and transitions in the upper row of Figure 1 and the data type part (AHON SIG, X , AHL) (see Section 3). The AHO net system consists of two places net holding AHL net systems and rules holding transformation rules. It allows on the one hand to trigger firing steps and on the other hand to apply rule based trans- formation steps for the object net system firing the transitions token firing and net transformation as indicated by the net in- scriptions fire(n,tσ ) and transform(rl, m), respectively. The execution of the workflow is con- trolled by firing the transitions on the sys- tem level. To start the activities of the firefighter team the transition Call the gas company is fired at the object level using the transition token firing at the system level. The result 1 Pipeline Emergencies Home Page http://pipeline.mindgrabmedia.com Proc. PNGT 2010 4 / 20 http://pipeline.mindgrabmedia.com ECEASST is the new AHL net system AHLNetSys′ = (AHLNet, M′) shown in Figure 2. Next we focus on the dynamic changes of the workflow at run time. The firefighters responsi- ble for the evacuation process need more detailed information how to proceed. To introduce the refinement of the Evacuate homes-transition into the AHL net system AHLNetSys′ we provide the rule AHLRule in Figure 1. y less 5 = tt Request to control traffic into the area Identify the location gas is highest Additional reading the gas indicator Shut off electricity and gas lines Reading the gas indicator Expand the area of evacuation p2:Tok gas company Call the Notify residents of the evacuation persons Assist handicapped the extent possible Guide persons to Deny entry Stand by p10:Nat y y p3:Tok p8:Tok p4:Tok p6:Tok p9:Tok p12:Tok p14:Tok p15:Tok p13:Tok p5:Tok p7:Tok x x x x x x x x x x x x x x x y x x x p11:Tok x x x x x p1:Tok x xx p’’:Tok p’:Tok x x x x x x Result >= 5% LEL y geq 5 = tt Result < 5% LEL Figure 3: AHLNetSys′′ The rule AHLRule = (L l← K r→ R) consists of the three AHL net systems L, K, and R, called left-hand side, inter- face, and right-hand side, respectively. The marking of the AHL net system L demands that the evacuation process is not yet started because there is one to- ken in the pre domain of the Evacuate homes-transition. To apply the rule AHLRule to the object net AHLNetSys, the transition net transformation is fired at the sys- tem level. The application of the rule refining the Evacuate homes-transition is achieved as follows: First, the match morphism m identifies the rele- vant parts of the left hand side L of the rule AHLRule in the AHL net system AHLNetSys′. As a next step, the Evac- uate homes-transition is deleted and we obtain an intermediate AHL net system. Afterwards, the transitions Notify resi- dents, Assist handicapped persons, and Guide persons together with their (new) environments are added to the interme- diate system leading to the new AHL net system AHLNetSys′′ shown in Figure 3. Thus we obtain the rule based transfor- mation AHLNetSys′ =⇒ AHLNetSys′′ via (AHLRule, m) and the result of fir- ing the transition net transformation at the system level is the replacement of the AHL net system AHLNetSys′ by AHLNetSys′′ on the place net. Afterwards, the firefighter company proceeds with its activities. The gas company has entered the area. After the identification of the problem the odor of gas grows stronger and the gas company personnel take an additional reading of the gas indicator. Immediately afterwards the gas company personnel inform the company officer about the lower explosive limit (LEL) such 5 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems that he is able to determine the isolation perimeter. Note that these activities depend on the exchange of messages and data concerning the result of reading the gas indicator and the final analysis of these results by the company officer. In this paper, we restrict the initial marking of the AHL net system AHLNetSys to one object net system and one corresponding rule to help the reader focus on the main concepts. In our example, only a predefined refinement of the object net system is applicable. Such a situation may be useful for modeling purposes or to show properties of a small object net, which is then transformed using rules that preserve these properties. But in general, different rules are avail- able which are applicable depending on the state of the object net. Their application can be further restricted by application conditions on the rule level or additional firing conditions for the transitions on the system level. Moreover, new rules may be added at runtime which allow to handle unforeseen events. For a full description of the emergency scenario, more object net systems and rules should be defined as, e. g., those given in [BRHM06, PHE+07]. 3 AHO Net Systems with High- and Low-Level Tokens In this section, we introduce our formal framework for modeling data-dependent workflows in mobile ad-hoc networks as motivated by the emergency scenario in Section 2. For this purpose, we introduce algebraic higher-order (AHO) net systems which allow algebraic high-level (AHL) net systems and rules as tokens. This extends our approach in [HME05] where we used AHO net systems with P/T systems and rules as tokens. AHL net systems resp. P/T systems are nets together with initial markings. These and the corresponding rules are used as tokens to model the interaction of token firing and net transformations. 3.1 Review of the Categories PTSys and AHLNetSys In the following, we review the category PTSys of P/T systems [HME05] and the category AHLNetSys of AHL net systems [Pra08], which are used as tokens for the corresponding AHO net systems. We use the notation of Petri nets as monoids [MM90], where a P/T net is defined by PT Net = (P, T, pre, post) with pre and post domain functions pre, post : T → P⊕. A P/T system is given by PT Sys = (PT Net, M) with a P/T net PT Net and a marking M ∈ P⊕, where P⊕ is the free commutative monoid over the set P of places with binary operation ⊕. More- over, each function f : A → B can be extended to a monoid homomorphism f⊕ : A⊕ → B⊕ with f⊕(∑a∈A kaa) = ∑a∈A ka f (a). Note that M can also be considered as a function M : P → N where only for a finite set P′ ⊆ P we have M(p) ≥ 1 with p ∈ P′. We can switch between these notations by defining ∑p∈P M(p)· p = M ∈ P⊕ and M(p) = ap for M = ∑p∈P ap p ∈ P⊕. Moreover, for M1, M2 ∈ P⊕ we have M1 ≤ M2 if M1(p) ≤ M2(p) for all p ∈ P. Note that the inverse of ⊕ is only defined in M1 M2 if M2 ≤ M1. Definition 1 (Category PTSys of P/T Systems) Given P/T systems PT Sysi = (PT Neti, Mi) with PT Neti = (Pi, Ti, prei, posti) for i = 1, 2, a P/T system morphism f : PT Sys1 → PT Sys2 is given by f = ( fP, fT ) with functions fP : P1 → P2 and fT : T1 → T2 satisfying Proc. PNGT 2010 6 / 20 ECEASST (1) f⊕P ◦ pre1 = pre2 ◦ fT and f ⊕ P ◦ post1 = post2 ◦ fT (2) M1(p) ≤ M2( fP(p)) for all p ∈ P1 Moreover, f is called strict if fP and fT are injective and (3) M1(p) = M2( fP(p)) for all p ∈ P1. The category defined by P/T systems and P/T system morphisms is denoted by PTSys where the composition and identities are defined componentwise for places and transitions. P/T systems are called low-level nets due to the fact that the tokens are indistinguishable. In contrast, a high-level net may hold different kinds of tokens and the firing behavior depends on the token kind. In AHL systems, the tokens are data elements and thus distinguishable. Definition 2 (Category AHLNetSys of AHL Net Systems) An algebraic high-level (AHL) net system AHLNetSys = (AHLNet, M) with AHLNet = ((SIG, X ), P, T, pre, post, cond,type, A) consists of an algebraic signature SIG = (sorts, opns) with sorts and operation symbols, addi- tional variables X , sets of places P and transitions T , pre and post domain functions pre, post : T →(TSIG(X )⊗P)⊕, firing conditions cond : T →P f in(Eqns(SIG; X )), a typing of places type : P → sorts, a SIG-algebra A, and an initial marking M ∈CP⊕. TSIG(X ) is the term algebra with variables over X , TSIG(X )⊗P = {(term, p)|term ∈ TSIG(X )type(p), p ∈ P}, Eqns(SIG; X ) are all equations over the signature SIG with variables X , and CP = A⊗P ={(a, p)|a∈Atype(p), p∈P}. Given AHL net systems AHLNetSysi = (AHLNeti, Mi) with AHLNeti = ((SIG, X ), Pi, Ti, prei, posti, condi,typei, A) for i = 1, 2, an AHL net system morphism f : AHLNetSys1 →AHLNetSys2 is given by f = ( fP, fT ) with functions fP : P1 → P2 and fT : T1 → T2 satisfying (1) (id ⊗ fP)⊕◦ pre1 = pre2 ◦ fT and (id ⊗ fP)⊕◦ post1 = post2 ◦ fT , (2) cond2 ◦ fT = cond1 (3) type2 ◦ fP = type1 (4) ∀a ∈ Atype1(p1), p1 ∈ P1 : M1(a, p1) ≤ M2(a, f p(p1)) Moreover, f is called strict if fP and fT are injective and (5) M1(a, p1) = M2(a, fP(p1)) for all a ∈ Atype1(p1) and p1 ∈ P1. The category defined by AHL net systems and AHL net system morphisms is denoted by AHLNetSys where the composition and identities are defined componentwise for places and transitions. For the firing of a transition in an AHL net system, we first have to find a suitable variable as- signment such that for the term inscription on the pre arc, tokens on the corresponding predomain places are selected satisfying the firing condition. 7 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems Definition 3 (Firing Behavior of AHL Net Systems) Given an AHL net system AHLNetSys = (AHLNet, M) with AHLNet = ((SIG, X ), P, T, pre, post, cond,type, A), the set of variables Var(t) ⊆ X of a transition t ∈ T are the variables of the net inscriptions in pre(t), post(t), and cond(t). Let σ : Var(t) → A be a variable assignment with term evaluation σ # : TSIG(Var(t)) → A, then (t, σ ) is a consistent transition assignment iff cond(t) is valid in A under σ . The set CT of consis- tent transition assignments is defined by CT = {(t, σ )|(t, σ ) consistent transition assignment}. A transition t ∈ T is enabled in M under σ iff (t, σ ) ∈ CT and preA(t, σ ) ≤ M, where preA : CT → CP⊕ is defined for pre(t) = ∑ni=1(termi, pi) by preA(t, σ ) = ∑ n i=1(σ #(termi), pi), and similarly for postA(t, σ ). Then the follower marking is computed by M′ = M preA(t, σ )⊕ postA(t, σ ). Intuitively, a pushout in the categories PTSys and AHLNetSys means the gluing of two net systems along an interface system. The pushout object is constructed componentwise for tran- sitions and places in the category SET with corresponding pre and post domain functions and initial markings. Definition 4 (Pushouts in the category PTSys) The pushout (PN2, M2) n→ (PN3, M3) g ← (PN1, M1) of the P/T system morphisms m : (PN0, M0) → (PN1, M1) and f : (PN0, M0) → (PN2, M2), where m is strict, can be constructed as pushout in PTNet [EP04], i.e. component-wise for places and transitions. The marking M3 is defined by 1. ∀p1 ∈ P1 \m(P0) : M3(gP(p1)) = M1(p1) 2. ∀p2 ∈ P2 \ f (P0) : M3(nP(p2)) = M2(p2) 3. ∀p0 ∈ P0 : M3(nP ◦ fP(p0)) = M2( fP(p0)) for Pi being the sets of places of PNi for i = 0, 1, 2, 3. Definition 5 (Pushouts in the category AHLNetSys) The pushout (AHLNet2, M2) n→ (AHLNet3, M3) g ← (AHLNet1, M1) of the AHL net system morphisms m : (AHLNet0, M0) → (AHLNet1, M1) and f : (AHLNet0, M0) → (AHLNet2, M2), where m is strict, can be constructed as pushout in AHLNet [PER95], i.e. componentwise for places and transitions. The marking M3 is defined by 1. ∀p1 ∈ P1 \m(P0), a ∈ Atype1(p1) : M3(a, gP(p1)) = M1(a, p1) 2. ∀p2 ∈ P2 \ f (P0), a ∈ Atype2(p2) : M3(a, nP(p2)) = M2(a, p2) 3. ∀p0 ∈ P0, a ∈ Atype0(p0) : M3(a, nP ◦ fP(p0)) = M2(a, fP(p0)) for Pi being the places of AHLNeti for i = 0, 1, 2, 3. Remark 1 Note that Items 2 and 3 combined are equivalent to ∀p2 ∈ P2, a ∈ Atype2(p2) : M3(a, nP(p2)) = M2(a, p2). Proc. PNGT 2010 8 / 20 ECEASST 3.2 AHO Net Systems with AHL Net Systems as Tokens An algebraic higher-order (AHO) net system can be considered as an algebraic high-level (AHL) net system modeling the system level. The main difference is that an AHO net system contains not an algebra, but a class algebra, i.e. an algebra with classes instead of sets as base sets. This specific class algebra A defines net systems and rules as tokens at the object level. The class algebra A includes domains like ANet , which is the class of all net systems of a specific kind of low-level or high-level net systems and cannot be restricted to be a set. In the following, we introduce AHO net systems which have AHL net systems and corresponding rules as tokens. First we introduce an algebraic signature for the class algebra of AHO net systems which can be used for low-level and high-level net systems as tokens, the enabling and firing of transitions as well as the applicability of rules, and the rule based transformation of net systems. Definition 6 (Signature for AHO Net Systems) The signature for algebraic higher order (AHO) net systems with net systems and rules as tokens is given by: AHON SIG = sorts: Net, Trans, Bool, Mor, Rules opns: undefined :→ Net, tt, ff :→ Bool, enabled : Net ×Trans → Bool, fire : Net ×Trans → Net, applicable : Rules×Mor → Bool, transform : Rules×Mor → Net cod : Mor → Net Note that the signature AHON SIG does not fix the type of net systems which may be used as tokens. This is achieved by the corresponding class algebras AHL for AHL net systems and APT for P/T systems as tokens, which are both class algebras for the signature AHON SIG. For AHL, (AHL)Net is the class of all AHL net systems AHLNetSys including a special undefined element specified by a constant. In order to model the consistent transition assign- ments of AHL net systems we define the domain (AHL)Trans to be the class Sets of all sets. Note, however, that only sets s of the form s = {(t, σ )} with (t, σ ) ∈CTAHL are relevant, where CTAHL is the set of all consistent transition assignments, t ∈ TAHL is a transition and σ : Var(t) → DAHL a corresponding variable assignment of some AHL net system AHLNetSys = ((SIGAHL, XAHL), PAHL, TAHL, preAHL, postAHL, condAHL,typeAHL, DAHL, MAHL). For the definition of the opera- tions enabledHL and fireHL we use the extended pre and post domain functions preDAHL and postDAHL (see Definition 3). In order to model the applicability of rules and rule based transformations of AHL net systems [Pra08] we use the operations applicableHL and transformHL defined on the domains (AHL)Mor of all AHLNetSys-morphisms and (AHL)Rules of all rules rl = (L l← K r→ R) for AHL net systems. A rule rl is applicable to AHLNetSys′ via match morphism m : AHLNetSys → AHLNetSys′ if L = AHLNetSys and m satisfies the gluing condition w.r.t. rl, which means that we have a pushout complement AHLNetSys0 in (1) below. In this case, we can construct the pushout (2) leading to AHLNetSys′′. The double pushout (1+2) defines the rule based transformation 9 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems AHLNetSys′ ⇒ AHLNetSys′′ via (rl, m). Note that due to the fact that pushouts are only unique up to isomorphism, we have to fix a concrete construction for the definition of transformHL selecting a specific pushout for each transformation according the one in Definition 5. L m �� (1) K loo r // �� R �� (2) AHLNetSys′ AHLNetSys0oo // AHLNetSys′′ Definition 7 (Class Algebra AHL for AHL Net Systems as Tokens) Given the signature AHON SIG, the class algebra AHL for AHL net systems and corresponding rules as tokens is given by AHL = ((AHL)Net , (AHL)Trans, (AHL)Bool , (AHL)Mor, (AHL)Rules, undefinedHL, ttHL, ff HL, enabledHL, fireHL, applicableHL, transformHL) with (AHL)Net = {AHLNetSys | AHLNetSys is an AHL net system}∪{unde f} the class of all AHL net systems including undefined, (AHL)Trans = Sets the class of all sets, (AHL)Bool = {true, false}, (AHL)Mor = {m : AHLNetSys → AHLNetSys′ | m AHLNetSys-morphism}, (AHL)Rules = {rl = (L l← K r→ R) | l, r strict AHLNetSys-morphisms}, undefinedHL = undef , ttHL = true, ff HL = false, enabledHL : (AHL)Net ×(AHL)Trans → (AHL)Bool defined for s ∈ (AHL)Trans by enabledHL(undef , s) = false and for AHLNetSys = ((SIGAHL, XAHL), PAHL, TAHL, preAHL, postAHL, condAHL, typeAHL, DAHL, MAHL) by enabledHL(AHLNetSys, s) =   true if ∃t, σ : s = {(t, σ )},t ∈ TAHL, (t, σ ) ∈CTAHL preDAHL (t, σ ) ≤ MAHL false else fireHL : (AHL)Net ×(AHL)Trans → (AHL)Net with fireHL(undef , s) = undef and for AHLNetSys = (AHLNet, MAHL) with fireHL(AHLNetSys, s) =   (AHLNet, M′AHL) if enabledHL(AHLNetSys, s) = true, s = {(t, σ )}, M′AHL = MAHL preDAHL (t, σ )⊕ postDAHL (t, σ ) undef else applicableHL : (AHL)Rules ×(AHL)Mor → (AHL)Bool with applicableHL(rl, m) = { true if L = AHLNetSys∧m satisfies gluing condition w.r.t. rl false else where rl = (L l← K r→ R) and m : AHLNetSys → AHLNetSys′ Proc. PNGT 2010 10 / 20 ECEASST transformHL : (AHL)Rules ×(AHL)Mor → (AHL)Net with transformHL(rl, m) =   AHLNetSys′′ if applicableHL(rl, m) = true and AHLNetSys′ (rl,m) =⇒ AHLNetSys′′ undef else codHL : (AHL)Mor → (AHL)Net with codHL(m) = AHLNetSys ′ for m : AHLNetSys → AHLNetSys′. Now we are able to define AHO net systems with AHL net systems and rules as tokens and the corresponding category AHONAHL. An AHO net system is defined using a “class algebra based” AHL net system, i.e. an AHL net system AHONAHL in the sense of Definition 2, where the algebra A is allowed to be a class algebra like AHL in Definition 7. But note that the carrier set (AHL)Net does not include class based AHL net systems like itself to avoid set theoretical problems of self inclusion. Definition 8 (Category AHONAHL of AHO Net Systems) Given the signature AHON SIG (see Definition 6) and the class algebra AHL (see Definition 7), an AHO net system AHONAHL – with AHL net systems and rules as tokens – is a (class algebra based) AHL net system AHONAHL = ((AHON SIG, X ), P, T, pre, post, cond,type, AHL, MHL) where the signature AHON SIG with sufficiently large family of sets X of variables and algebra AHL are fixed. The initial marking MHL ∈(AHL⊗P)⊕ can be represented by MHL : AHL⊗P →N. A morphism f : AHON1AHL → AHON2AHL of AHO net systems is an AHLNetSys-morphism. This means that for AHO net systems AHONiAHL = ((AHON SIG, X ), Pi, Ti, prei, posti, condi, typei, AHL, MiHL ) for i = 1, 2, we have f = ( fP : P1 → P2, fT : T1 → T2) with (=) T1cond1 sshhhhh hhhh hhhh h fT �� pre1 // post1 // (=) (TAHON SIG(X )⊗P1)⊕ (id⊗ fP)⊕ �� P f in(Eqns(AHON SIG, X )) T2 cond2 kkWWWWWWWWWWWWWW pre2 // post2 // (TAHON SIG(X )⊗P2)⊕ P1 fP �� type1 **TTT TTTT TTT (=) sorts(AHON SIG) P2 type2 44jjjjjjjjjj and M1HL (a, p1) ≤ M2AHL (a, fP(p1)) for all p1 ∈ P1 and a ∈ (AHL)type1(p1). The category AHONAHL of AHO net systems based on the class algebra AHL consists of all AHO net systems as objects and AHO net system morphisms as morphisms. Example 1 (AHO Net System for Emergency Scenario) The AHO net system AHONAHL = ((AHON SIG, X ), P, T, pre, post, cond,type, AHL, MHL) in Figure 1 consists of 11 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems • the signature AHON SIG (see Definition 6), the AHON SIG-algebra AHL (see Defini- tion 7), and variables XNet = {n}, XTrans = {tσ}, XBool = ∅, XMor = {m}, XRules = {rl}, • the set of places P = {net, rules} with type(net) = Net and type(rules) = Rules, • the set of transitions T = {token firing, net transformation} with pre and post domain and firing conditions as shown in Figure 1, and • the initial marking MHL = (AHLNetSys, net)⊕(AHLRule, rules), where AHLNetSys and AHLRule are shown as marking on the places net and rules, respectively. The data type part of the AHL net systems AHLNetSys and L, K and R in AHLRule is given by the signature and corresponding algebra of natural numbers and boolean values together with a sort Tok for black tokens. As shown in [Pra08] for algebraic high-level net systems with fixed data type, the category AHONAHL is a weak adhesive HLR category where pushouts are constructed componentwise, because the fact that AHL is a class algebra instead of a classical algebra does not affect these properties. 3.3 AHO Net Systems with P/T Systems as Tokens In order to define a net class transformation from AHO net systems with high-level net system and rules as tokens to those with low-level net systems and rules as tokens we briefly introduce the second kind of AHO net system. In fact, we can use the same signature AHON SIG (see Definition 6) but use a different class algebra APT for P/T systems and corresponding rules as tokens. APT = ((APT )Net , (APT )Trans, (APT )Bool , (APT )Mor, (APT )Rules, undef , true, false, enabledPT , firePT , applicablePT , transformPT ) The main difference is that (APT )Net is the class of all P/T systems (including a constant for undefined) and (APT )Mor, (APT )Rules as well as applicablePT and transformPT are based on PTSys-morphisms instead of AHLNetSys-morphisms (see Definition 7). The operations enabledPT and firePT are defined for P/T systems PT Sys = (PT Net, MN ) = (PN , TN , preN , postN , MN ) and a set s ∈ (APT )Trans by enabledPT : (APT )Net ×(APT )Trans → (APT )Bool with enabledPT (undef , s) = false, enabledPT (PT Sys, s) = { true if ∃t ∈ TN : s = {t} and preN (t) ≤ MN false else firePT : (APT )Net ×(APT )Trans → (APT )Net with firePT (undef , s) = undef and firePT (PT Sys, s) =   (PT Net, M′N ) if enabledPT (PT Sys, s) = true with s = {t} and M′N = MN preN (t)⊕ postN (t) undef else Proc. PNGT 2010 12 / 20 ECEASST This class algebra leads to AHO net systems AHONPT with P/T systems and rules as tokens and to the corresponding category AHONPT. Note that our class algebra APT is more general than the one in [HME05], where (APT )Net is restricted to all P/T systems which are subsystems of a given super net system. Definition 9 (Category AHONPT of AHO Net Systems) Given the signature AHON SIG (see Definition 6) and the class algebra APT , an AHO net system AHONPT with P/T systems and rules as tokens is a (class algebra based) AHL net system AHONPT = ((AHON SIG, X ), P, T, pre, post, cond,type, APT , MPT ) with fixed (AHON SIG, X ) and APT . Together with corresponding AHL net system morphisms we obtain the category AHONPT of AHO net systems based on class algebra APT . Example 2 An example of an AHO net system with P/T systems and rules as tokens is de- picted in Figure 4, which is analogously defined to the AHO net system AHONAHL in Figure 1, but the AHON SIG-algebra is given by APT and the initial marking by MPT = (PT Sys, net)⊕ (PT Rule, rules), where PT Sys is a P/T system and PT Rule a P/T system rule. 4 Net Class Transformation for AHO Net Systems Since several net classes form different categories, net class transformations are expressed by functors. Well-known examples of net class transformations are the concepts of flattening and skeleton as introduced in [Urb03]. In this section, the extended skeleton of AHO net systems is introduced. It is expressed by the functor FSkel : AHONAHL → AHONPT based on the skeleton functor Skel : AHLNetSys → PTSys. Both functors are defined and some interesting properties of the functor FSkel are verified. 4.1 Extended Skeleton Functor for AHO Net Systems The functor FSkel : AHONAHL → AHONPT extends the skeleton functor Skel : AHLNetSys → PTSys (see [Urb03]) that “forgets” the data type of an AHL net system but preserves the token count on the places and the multiplicity of the edges. Definition 10 (Functor Skel) Given the AHL net system AHLNetSys = ((SIG, X ), P, T, pre, post, cond,type, A, M) and a morphism f = ( fP, fT ) : AHLNetSys → AHLNetSys′, the skeleton functor Skel : AHLNetSys → PTSys is defined by Skel(AHLNetSys) = PT Sys = (P, T, pre′, post′, M′) Skel( f ) = f ′ : Skel(AHLNetSys) → Skel(AHLNetSys′) with pre′(t) = πP⊕(pre(t)), post ′(t) = πP⊕(post(t)) for all t ∈ T , where πP⊕ : (TSIG(X )⊗P)⊕→ P⊕ is a projection, M′(p) = ∑a∈Atype(p) M(a, p), and f ′ P(p) = fP(p) and f ′ T (t) = fT (t) for all p ∈ P and t ∈ T . 13 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems Result < 5% LEL Request to control traffic into the area Identify the location gas is highest Additional reading the gas indicator Shut off electricity and gas lines gas company Call the Reading the gas indicator Expand the area of evacuation Notify residents of the evacuation persons Assist handicapped the extent possible Guide persons to Deny entry Stand by p10 Evacuate homes in the immediate area p1 4p3p p6 p9 p12 p14 p15 p13 p8 p p’’’ p’’ p’ R p p’’’ K rl the immediate area Evacuate homes in p p’’’ L p7 p5 p2 p11 Result >= 5% LEL n m : Mor cod m = n applicable(rl, m) = tt n tσ : Trans token firing transform(rl, m) net transformation rl rules : Rules (AHON SIG, X ), APT enabled(n,tσ ) =tt net : Net fire(n,tσ ) PTSys PTRule Figure 4: Algebraic higher-order net system AHONPT Remark 2 The skeleton functor Skel : AHLNetSys → PT Sys preserves pushouts, double- pushout (DPO) transformations, and also enabling and firing of transitions. The extended skeleton functor FSkel for AHO net systems “forgets” the data type part of the object net systems using the skeleton functor Skel. Moreover, this functor replaces the AHON SIG-algebra AHL for AHL net systems and the corresponding rules by the algebra APT for P/T systems and the corresponding skeleton rules. Definition 11 (Functor FSkel ) Given the AHO net system AHONAHL = ((AHON SIG, X ), P, T, pre, post, cond, type, AHL, MHL) with fixed class algebra AHL (see Definition 7) and MHL : AHL ⊗P → N then the extended skeleton functor FSkel : AHONAHL → AHONPT is given by Proc. PNGT 2010 14 / 20 ECEASST FSkel (AHONAHL) = AHONPT = ((AHON SIG, X ), P, T, pre, post, cond,type, APT , MPT ) with fixed class algebra APT (see Subsection 3.3) and MPT : APT ⊗P → N defined by (∗) MPT (aPT , p) = ∑ aHL∈(AHL)type(p) ∑ Stype(p)(aHL)=aPT MHL(aHL, p) for aPT ∈ APT , aHL ∈ AHL, and S : AHL → APT defined as family S = [Ss : (AHL)s → (APT )s]s∈Y for Y = {Net, Trans, Bool, Mor, Rules} is given for a ∈ (AHL)s by Ss(a) =   Skel(a) for s ∈{Net, Mor, Rules} undef for s = Net, a = undef {t} for s = Trans and a = {(t, σ )} with t ∈ T a for (s = Trans and a 6= {(t, σ )} with t ∈ T ), or s = Bool For a morphism f = ( fP, fT ) : AHONAHL → AHON′AHL of AHO net systems it is defined by FSkel ( f ) = f ′ : AHONPT → AHON′PT with f ′ = ( fP, fT ). Remark 3 Note that S : AHL → APT defined above by the family [Ss]s∈Y is not an AHONSIG- homomorphism since it is not compatible with the enable-operations as shown in the introduction of the Subsection 4.2. In the following theorem, we show that FSkel is a functor and preserves pushouts along strict morphisms and transformations. Theorem 1 1. FSkel : AHONAHL → AHONPT is functor. 2. FSkel preserves pushouts along strict morphisms and double pushout transformations. Proof. 1. From the definition, it is clear that FSkel is compatible with composition and identities. Mainly, we have to show that it is well-defined for the marking, i.e. for f : AHON1AHL → AHON2AHL in AHONAHL with M1HL (aHL, p) ≤ M2HL (aHL, fP(p)) we have to show that M1PT (aPT , p) ≤ M2PT (aPT , fP(p)) for FSkel ( f ) : FSkel (AHON1AHL ) → FSkel (AHON2AHL ) in AHONPT. Using (*) in Definition 11 in Section 4 we have that M1PT (aPT , p) = ∑ S(aHL)=aPT M1HL (aHL, p) ≤ ∑ S(aHL)=aPT M2HL (aHL, fP(p)) = M2PT (aPT , fP(p)) 15 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems 2. First, we show that FSkel preserves pushouts along strict morphisms. Let AHONiAHL = (ANiAHL , MiHL ) for i = 0, 1, 2, 3 and (1) be a pushout in AHONAHL (see Definition 5) along the strict morphism f1. (AN0AHL , M0HL ) f1 // f2 �� (1) (AN1AHL , M1HL ) g1 �� (AN2AHL , M2HL ) g2 // (AN3AHL , M3HL ) (AN0PT , M0PT ) f1 // f2 �� (2) (AN1PT , M1PT ) g1 �� (AN2PT , M2PT ) g2 // (AN3PT , M3PT ) Applying FSkel we obtain AHONiPT = (ANiPT , MiPT ) in (2) with ANiPT obtained from ANiAHL by replacing AHL by APT . We have to show that (2) is a pushout in AHONPT(see Defini- tion 4). According to the pushout construction in AHLNetSys (see Definition 5) along the strict morphism f1 in (1) we have that MiHL (i = 0, 1, 2, 3) with M3HL (aHL, g1(p1)) = M1HL (aHL, p1) for p1 ∈ P1\ f1(P0) and M3HL (aHL, g2(p2)) = M2HL (aHL, p2) for p2 ∈ P2. By definition of FSkel we have MiPT (aPT , p) = ∑ S(aHL)=aPT MiHL (aHL, p) for i=0,1,2, 3, where Pi are the places of ANiHL resp. ANiPT . It remains to show that M3PT (aPT , g1(p1)) = M1PT (aPT , p1) for p1 ∈ P1\ f1(P0) and M3PT (aPT , g2(p2)) = M2PT (aPT , p2) for p2 ∈ P2. For p1 ∈ P1\ f1(P0), we have that M3PT (aPT , g1(p1)) = ∑ S(aHL)=aPT M3HL (aHL, g1(p1)) = ∑ S(aHL)=aPT M1HL (aHL, p1) = M1PT (aPT , p1) Similarly, M3PT (aPT , g2(p2)) = M2PT (aPT , p2) for all p2 ∈ P2. Hence, (2) is a pushout in AHONPT which implies that FSkel preserves pushouts along strict morphisms. This also implies that FSkel preserves double pushout transformations. Proc. PNGT 2010 16 / 20 ECEASST 4.2 Firing Properties of the Net Class Transformation In this subsection, we analyze under which conditions the net class transformation FSkel : AHONAHL → AHONPT preserves enabling and firing of transitions at the system level. As explained above, h : AHL →APT based on the skeleton functor Skel : AHLNetSys→PTSys is not a homomorphism because this functor preserves the firing behavior, but in general it does not reflect enabling and firing of transitions. This means that enabledHL(AHLNetSys,{(t, σ )}) = b implies enabledPT (Skel(AHLNetSys)),{t}) = b for b = true but not for b = false. Definition 12 (Firing Properties of FSkel ) Given an AHO net system AHONAHL = ((AHON SIG, X ), P, T, pre, post, cond,type, AHL, MHL) with FSkel (AHONAHL) = AHONPT we say that FSkel preserves 1. consistent transition assignments, if ∀t ∈ T, σ : Var(t) → AHL: (t, σ ) ∈CTAHL ⇒ (t, σ ′) ∈CTPT for σ ′ = S◦σ 2. enabling, if ∀(t, σ ) ∈CTAHL: preAHL (t, σ ) ≤ MHL ⇒ preAPT (t, σ ′) ≤ MPT = (S⊗idP)⊕(MHL) 3. firing, if for MHL enabled under (t, σ ) ∈CTAHL: M′HL = MHL preAHL (t, σ )⊕ postAHL (t, σ ) ⇒ M′PT = (S⊗idP)(M ′ HL) = MPT preAPT (t, σ ′)⊕ postAPT (t, σ ′) Remark 4 In general, the functor FSkel : AHONAHL → AHONPT does not preserve consistent transition assignments, especially if cond(t) includes an equation of the form enabled(n,tσ ) = ff (see introduction of Subsection 4.2). But FSkel preserves consistent transition assignments if cond(t) includes only special equations of the form enabled(n,tσ ) = tt, fire(n,tσ ) = n′, applicable(rl, m) = tt, transform(rl, n) = n′, and cod(m) = n. In this case, Skel preserves en- abling, firing, pushouts, DPO-transformations (see Remark 2), and codomains. Theorem 2 (Firing Properties of FSkel ) For an AHO net system AHONAHL, FSkel : AHONAHL → AHONPT preserves enabling and firing if it preserves consistent transition assignments. Proof. Suppose that the arc inscriptions of AHONAHL are only variables or sums of variables. If this is not the case, we modify the AHO net system by introducing for each term tm in the arc inscriptions a new variable x and an equation x = tm for the corresponding transition. For all t ∈ T , σ : Var(t) → AHL we have that (t, σ ) ∈ CTAHL implies (t, σ ′) ∈ CTPT for σ ′ = S◦σ . 1. FSkel preserves enabling. For (t, σ ) ∈CTAHL and preAHL(t, σ ) ≤ MHL we have that preAPT (t, σ ′) (∗∗) = (S⊗idP)(preAHL (t, σ )) ≤ (S⊗idP)(MHL) = MPT 17 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems where (**) holds because pre(t) = ∑ni=1(termi, pi) and σ : Var(t) → AHL implies preAHL (t, σ ) = n ∑ i=1 (σ #(termi), pi) and preAPT (t, σ ′) = n ∑ i=1 (σ ′#(termi), pi) = (S⊗idP)( n ∑ i=1 (σ #(termi), pi)) = (S⊗idP)(preAPT (t, σ )) Note that σ ′ = S◦σ implies σ ′#(termi) = S(σ #(termi)) because by assumption the arc inscriptions termi are only variables. Otherwise we would need S : AHL → APT to be an AHON SIG-homomorphism which is not true in general. 2. FSkel preserves firing. M′PT = (S⊗idP)(M ′ HL) = (S⊗idP)(MHL preAHL (t, σ )⊕ postAHL (t, σ )) = (S⊗idP)(MHL) (S⊗idP)(preAHL (t, σ ))⊕ (S⊗idP)(postAHL (t, σ )) = MPT preAPT (t, σ ′)⊕ postAPT (t, σ ′) Example 3 The result of the extended skeleton functor FSkel applied to the AHO net system AHONAHL in Figure 1 is the AHO net system AHONPT = ((AHON SIG, X ), P, T, pre, post, cond,type, APT , MPT ) with P/T system and rule tokens in Figure 4. The firing conditions of AHONAHL in Figure 1 consist only of equations of the form enabled(n, tσ ) = tt, applicable(rl, m) = tt, and cod(m) = n so that consistent transition assignments are pre- served by the extended skeleton functor (see Remark 4). Moreover, by Remark 4 we obtain new equations of the form fire(n,tσ ) = n′ and transform(rl, n) = n′ if we replace the arc inscrip- tions fire(n,tσ ) and transform(rl, n) by n′ and introduce the new equations as conditions for the transitions token firing and net transformation, respectively. According to Remark 4, FSkel still preserves consistent transition assignments including also there new equations. Hence, we can assume without loss of generality that the arc inscriptions of AHONAHL in Figure 1 on the sys- tem level are only variables. Thus, due to Theorem 2, the enabling and firing of AHONAHL in Figure 1 is preserved by FSkel . In more detail, consider the consistent transition assignment (token firing, σ ) with σ (n) = AHLNetSys and σ (tσ ) be the consistent transition assignment of the object net system AHLNetSys given by the Call the gas company-transition and corresponding variable assign- ment and M′HL be the follower marking of AHONAHL (see Figure 2). Then (token firing, σ ′) with Proc. PNGT 2010 18 / 20 ECEASST σ ′(n) = Skel(AHLNetSys) = PT Sys, σ ′(tσ ) = Call the gas company and PT Sys = (PT Net, M) is a consistent transition assignment of the AHO net system AHONPT (see Figure 4). Moreover, the transition token firing is enabled in AHONPT under σ ′ and the follower marking is defined by M′PT = (PT Sys ′, net)⊕(PT Rule, rules) with PT Sys′ = (PT Net, M′), where M′ is given by the marking of the three places in the post domain of the Call the gas company-transition. 5 Conclusion and Future Work In this paper, we have introduced AHO net systems, a special kind of algebraic high-level nets with net systems and corresponding rules as tokens. Moreover, we have analyzed the skeleton functor FSkel : AHONAHL → AHONPT relating AHO net systems based on AHL net systems to AHO net systems based on P/T nets. In [Urb03], net class transformations have been introduced to allow a model developer to change the underlying Petri net class during the modeling step. This concept has been applied on classes of marked place/transition nets and algebraic high-level nets. In addition to the func- tor Skel : AHLNetSys → PTSys we should analyze the functors F lat : AHLNetSys → PTSys and Data : PTSys → AHLNetSys as given in [Urb03] leading to corresponding functors FF lat : AHONAHL → AHONPT and FData : AHONPT → AHONAHL. The functor F lat : AHLNetSys → PTSys relates AHL net systems to P/T systems as well, but in contrast to Skel it preserves the data type information as each possible marking of the AHL net system is considered to be a place in the P/T system. The data type is flattened into the set of places, hence the name. The functor Data : PTSys → AHLNetSys lifts a P/T system to an AHL net system by providing a trivial data type that describes the black tokens. This functor preserves the net structure and adds a one-sorted specification and an algebra where the carrier set has only one element, that is the black token. Similar to [Urb03], the corresponding functors FF lat : AHONAHL → AHONPT and FData : AHONPT → AHONAHL formalize net class transformations at the level of tokens of an AHO net system. These net class transformations allow changes of the underlying Petri net class at the token level. The signature and algebra in this paper are tailored to our needs to represent MANETs with AHO net systems. But the underlying principles including the analysis using the skeleton func- tor can be transferred to other high-level systems based on additional sorts and operations. A more thorough analysis concerning the properties that are required for the algebra would be an interesting line of future work. Bibliography [vdA03] W. van der Aalst. The Application of Petri Nets to Workflow Management. Journal of Circuits, Systems and Computers 8(1):21–66, 2003. [AZ03] D. Agrawal, Q. Zeng. Introduction to Wireless and Mobile Systems. Thomson Brooks/Cole, 2003. 19 / 20 Volume 40 (2011) Functorial Analysis of Algebraic Higher-Order Net Systems [BRHM06] P. Bottoni, F. Rosa, K. Hoffmann, M. Mecella. Applying Algebraic Approaches for Modeling Workflows and their Transformations in Mobile Networks. Journal of Mobile Information Systems 2(1):51–76, 2006. [EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. EATCS Monographs. Springer, 2006. [EHP+07] H. Ehrig, K. Hoffmann, J. Padberg, U. Prange, C. Ermel. Independence of Net Transformations and Token Firing in Reconfigurable Place/transition Systems. In Proc. of ATPN 2007. LNCS 4546, pp. 104–123. Springer, 2007. [EP04] H. Ehrig, J. Padberg. Graph Grammars and Petri Net Transformations. In Lectures on Concurrency and Petri Nets Special Issue Advanced Course PNT. LNCS 3098, pp. 496–536. Springer, 2004. [HME05] K. Hoffmann, T. Mossakowski, H. Ehrig. High-Level Nets with Nets and Rules as Tokens. In Proc. of ATPN 2005. LNCS 3536, pp. 268–288. Springer, 2005. [MM90] J. Meseguer, U. Montanari. Petri Nets are Monoids. Information and Computation 88(2):105–155, 1990. [PEH07] J. Padberg, H. Ehrig, K. Hoffmann. Formal Modeling and Analysis of Flexible Pro- cesses in Mobile Ad-Hoc Networks. Bulletin of the EATCS 91:128–132, 2007. [PER95] J. Padberg, H. Ehrig, L. Ribeiro. Algebraic High-Level Net Transformation Sys- tems. MSCS 5:217–256, 1995. [PHE+07] J. Padberg, K. Hoffmann, H. Ehrig, T. Modica, E. Biermann, C. Ermel. Maintain- ing Consistency in Layered Architectures of Mobile Ad-Hoc Networks. In Proc. of FASE 2007. LNCS 4422, pp. 383–397. Springer, 2007. [Pra08] U. Prange. Towards Algebraic High-Level Systems as Weak Adhesive HLR Cate- gories. ENTCS 203(6):67–88, 2008. [RMPM03] F. Rosa, V. Martino, L. Paglione, M. Mecella. Mobile Adaptive Information Sys- tems on MANET: What We Need as Basic Layer? In Proc. of MMIS 2003. 2003. [Urb03] M. Urbášek. Categorical Net Transformations for Petri Net Technology. PhD thesis, TU Berlin, 2003. [Val98] R. Valk. Petri Nets as Token Objects: An Introduction to Elementary Object Nets. In Proc. of ATPN 1998. LNCS 1420, pp. 1–25. Springer, 1998. Proc. PNGT 2010 20 / 20 Introduction and Related Work Motivation: Emergency Scenario AHO Net Systems with High- and Low-Level Tokens Review of the Categories PTSys and AHLNetSys AHO Net Systems with AHL Net Systems as Tokens AHO Net Systems with P/T Systems as Tokens Net Class Transformation for AHO Net Systems Extended Skeleton Functor for AHO Net Systems Firing Properties of the Net Class Transformation Conclusion and Future Work