Ina Schaefer, Loek Cleophas, Michael Felderer (Eds.): Workshops at Modellierung 2018,, (Hrsg.): Petri Gesellschaft Lecture Notes in Informatics (LNI), Nets and Modeling 2018 (PeMod18) für Informatik, Bonn 20181671 Hierarchical, Reconfigurable Petri Nets Jan-Uriel Lorbeer, Julia Padberg1 Abstract: Hierarchical Petri nets allow a more abstract view whereas reconfigurable Petri nets model dynamic structural adaptation. In this contribution we present the combination of reconfigurable Petri nets and hierarchical Petri nets yielding an hierarchical structure for reconfigurable Petri nets. Hierarchies are established by substituting transitions by subnets. These subnets are themselves reconfigurable, so they are supplied with their own set of rules, so-called local rules. Moreover, global rules, that can be applied in all of the net, are provided. Keywords: reconfigurable Petri nets; Petri net transformations; hierarchical Petri nets 1 Introduction Modelling modern systems presents a lot of challenges some of which can be eased by the use of appropriate models. A well known technique for system modelling are Petri nets. Petri nets provide a graphical language for constructing system models as well as a precise, mathematical semantics. These models can be used for simulations and to analyse the model’s properties. This allows locating possible faults in the system at earlier stages which also can decrease overall development costs. The increasing sizes of modern systems results in models becoming rather large and possibly hard to comprehend. Additional abstraction layers as for example hierarchies present one solution for the increasing size. Hierarchical Petri nets use hierarchy to break down the complexity of a large model, by dividing it into a number of submodels. This helps to concentrate on a specific system part without the need to take the whole system into account. Also submodels can be reused with less effort at multiple locations in the same system or even in a different system where similar components are used. Advanced systems that need dynamic structural adaptation can be modelled using reconfig- urable Petri nets, an approach for dynamic changes in Petri nets. A reconfigurable Petri net consist of a Petri net and set of rules that modify the Petri net’s structure at runtime. Hence they increase flexibility enabling the modification of a net while allowing the transitions to fire. The characteristic feature of reconfigurable Petri nets is the possibility to discriminate between different levels of change as they consist of a Petri net and a set of rules that can modify the Petri net. They provide powerful and intuitive formalisms to model dynamic software or hardware systems that are increasingly executed in dynamic infrastructures. 1 Hamburg University of Applied Sciences, Hamburg, Germany, julia.padberg@haw-hamburg.de cbe 2168 Jan-Uriel Lorbeer, Lorbeer, Julia Padberg Padberg Such infrastructures are dynamic as they are themselves subject to change and support various applications that may or may not share some of the resources. Reconfigurable Petri nets have been used in many different application areas, that require both the representation of their processes and of the system changes within one model. Examples are concurrent systems [LO04], mobile ad-hoc networks [Pa07], workflows in dynamic infrastructures [HEP08], communication spaces [MGH10, GE12], ubiquitous computing [GNH12, Bo06], flexible manufacturing systems [Tâ12], reconfigurable manufacturing systems [KBD16]). In [PK18] a comprehensive overview of reconfigurable Petri nets is given, including theoretical foundations and application areas. The term reconfigurable Petri nets is used since the underlying type of Petri net may vary (for example being place/transition nets, object nets, timed and/or stochastic nets, or high-level nets). Hence, this approach can be considered a family of formal modelling techniques (see [PK18] for details). Reconfigurable Petri nets are an instantiation of abstract transformation systems, called M- adhesive transformations systems, that are formulated in category theory. The fundamental idea is to characterize those categories that allow double-pushout transformations: therefore only the diagrammatic descriptions are needed. This has the advantage of a thorough theory that yields a vast amount of results concerning the transformation part. Nevertheless, in this contribution we omit the categorical foundation. Hierarchical, reconfigurable Petri nets combine the hierarchical Petri net types and reconfig- urable Petri net types into one, allowing a focused design of submodels and their reusability and the ability for dynamic changes at runtime. The main idea is to use the hierarchies purely at the surface, so the semantics is defined in terms of the underlying flattened reconfigurable net. Main Concept: Hierarchy as a syntactic extension The hierarchy based on transitions being replaced by subnets is given as a syntactic abbreviation. The hierarchical reconfigurable net is defined purely by it’s flattening into a reconfigurable net. This fundamental design decision has the following advantages: First, only the consistency of the flattening construction can be guaranteed using well-known results, but no further semantic correctness needs to be proven. Second, this corresponds directly to the intended implementation of hierarchies in ReConNet [Re17, Pa12] (ReConfigurable Net). Moreover, the transformation systems needs not to be shown for another category of hierarchical nets. And, apart from the flattening construction, which needs to be done once, the analysis and verification of a hierarchical Petri net requires no more effort than it’s counter part with no hierarchy, since the whole behaviour is defined in terms of the flattened net. The software tool ReConNet has been developed so that the modelling and simulation capabilities of reconfigurable nets are supported adequately. The most important feature of the tool is the ability to create, modify and simulate reconfigurable nets in a single tool through an intuitive graphic-based user interface. It allows the design and verification of Hierarchical, Reconfigurable Hierarchical, PetriPetri Reconfigurable Nets 1693 Nets reconfigurable place/transition nets. In this paper we discuss the basis for the integration of hierarchical reconfigurable Petri nets in ReConNet. This paper is organised as follows: We start by given a very simple introductory example of hierarchical reconfigurable Petri nets in Sect. 2. In Sect. 3 related work, namely approaches to hierarchical Petri nets and hierarchical graph transformations are discussed. The subsequent section introduces reconfigurable place/transition nets with labels. Sect. 5 elaborates the formal definition of hierarchical reconfigurable Petri nets and their flattening, the definition of transformation rules and proves the correctness of the flattening construction. The integration of reconfigurable hierarchical Petri nets into the simulation tool for reconfigurable Petri nets ReConNetis discussed in Sect. 6. The conclusion in Sect. 7 completes this paper. 2 Introductory Example Reconfigurable Petri nets extend classical Petri nets to include the possibility of dynamic changes. This is achieved through the use of a rewriting system and allows the modification of the net’s structure at run time. Such a system provides two kinds of changes: • a change of state accomplished through the firing of the net’s transitions • a change of the process itself induced by the rules. A reconfigurable Petri net N can either fire an activated transition or execute a transformation r step N ⇒= M. An example for this process is displayed in Fig. 1. In Fig. 1a a reconfigurable Petri net N is shown and in Fig. 1b it’s rule r with r’s nets L, K and R is given. N consists of two places, two tokens and one transition which is black when activated. When rule r is executed the net’s arcs are inverted. In it’s initial state (1) the rule r is not executable because there is no match to the rule’s left-hand net L. The net L specifies that at least two tokens are required at the place P at the figure’s bottom where the edges lead to. So only the transition T can fire. Firing transition T twice state (3) is reached. In this state two tokens are located on the bottom place P and r can be executed inverting the arc directions resulting in state (4). If in state (3) there would have been an additional token on the upper place P either the transition T could have fired or r could have been executed. In state (4) r is no longer executable because the edges now lead to the upper place P, so only the transition T can fire. State (4) is very similar to state (1) and after T firing twice r would be executable once again. 4170 Jan-Uriel Lorbeer, Lorbeer, Julia Padberg Padberg (a) State sequence of net N (b) Rule r Fig. 1: Reconfigurable Petri net RN = (N, {r }) To give an intuition of hierarchical reconfigurable Petri nets we subsequently give an example that comprises the ideas presented in the following sections. Imagine some simple but adaptive process that can alternatively execute three different tasks task1, task2, and task3. An abstract view of this process is given in Fig. 2. Fig. 2: Abstract view: Net AN Fig. 3: Flattened net F L AT(AN) The tasks task2 and task3 are more complex and are given by subnets, where task2 is a sequence of steps and task3 includes some forking. The hierarchy concept in Sect. 5 allows the substitution of the transitions with the subnets. The substitution of the transition task2 replaces the transition and its adjacent places, that is Net(task2), by the subnet SN1 and Net(task3) is replaced by SN2, both in Fig. 4. Applying these substitutions to the abstract nets in Fig. 2 yields the flatted net in Fig. 3. Fig. 4: Substitution of transitions Hierarchical, Reconfigurable Hierarchical, PetriPetri Reconfigurable Nets 1715 Nets Now we add rules for the subnets for the adaptation of the tasks: task1 is so simple, it requires no adaptation. In task2 the sequence of steps can be changed (rules SN1:r1 and SN1:r2) or an intermediate steps is introduced or removed ( rules SN1:r3 and SN1:r4). So we have the four rules that belong to subnet SN1 and are given in light grey in Fig. 5. In task3 the intermediate step can be adapted by rule SN2:r5 so that parallel step may require something from the intermediate result. And this adaptation can be reversed by rule SN2:r6. Both rules belong to subnet SN2 and are given in dark grey in Fig. 5. These six rules are local rules, that should be only applied in the corresponding subnet. The transitions have the name space AT = {initialise, task1, task2, task3, fork, join, step, step1, step2, intermediate step, parallel step} that ensures the locality of the rules by the labels. Fig. 5: Local rules for the subnets SN1 and SN2 Additionally, we want a global rule that adds to all steps a counting place. This rule is given below in Fig. 6. This rule can be applied at each transition with a lesser label. The name space AT for the transition is ordered in the following way: gT ≥ l for all l ∈ AT and step ≥ l for all l ∈ {step1, step2, intermediate step, parallel step} which are the other local steps. Fig. 6: Global rule for adding counter 6172 Jan-Uriel Lorbeer, Lorbeer, Julia Padberg Padberg 3 Related Work The main related research areas for hierarchical reconfigurable Petri nets are obviously hierarchical Petri nets and hierarchical graph transformations. From 1991 on, hierarchies in Petri nets [HJS91] have been used in numerous papers and contributions and are still prominent, e.g. [HW18, Ak17]. In [HW18] the HiPS tool provides a common operating method, graphical user interface, the ability to describe hierarchical Petri nets and an on-the-fly linear temporal logic model checker. [Ak17] defines a hierarchy of places, and with various arcs as inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. A total ordering over the places encodes the hierarchy depending on the arc types various extensions are given. The decidability for almost all these extensions has been shown using different reductions and proof techniques. Besides hierarchical Petri nets based on transition substitution as e.g. in [JR91] nets based on place substitution and Object-Oriented Petri nets [La01, MK05] have been considered. CPN [CP17] also supports fusion places by defining sets of places that are functionally identical. The net-in-nets approach [Va98, Va04] as well as object nets [KH10, KH11] yield hierarchical composition as well. There are a number of tools similar to ReConNet. CPN tools [Ra03, CP17] is the main tool for the modelling and simulation of coloured Petri nets. Using a graphic user interface CPN tools features syntax checking, code generation and state space analysis. Snoopy [He12] is a unifying Petri net framework with a graphical user interface. It allows the modelling and simulation of coloured and uncoloured Petri nets of different classes, supports analytic tools and the hierarchical structuring of models. The HiPS tool [Hi17] developed at the Department of Computer Science and Engineering, Shinshu University is a tool written in C# and also employs a graphical user interface. HiPS is a platform for design and simulation of hierarchical Petri nets. It also provides functions of static and dynamic net analysis. While all of these tools support the design of hierarchical Petri nets it is evident that they lack reconfiguration, ReConNet’s core feature. Hierarchical graphs (and graph transformations) add some hierarchy to the nodes or to the edges. Various approaches to graphs with hierarchy have been proposed, e.g. [BH01, DHP02, BKK05, Br14]. The resulting techniques were used for modelling hierarchical hypermedia, distributed project management, mobile and ubiquitous systems among others. Hypergraphs in [DHP02] consist of two finite sets of nodes and hyperedges. The hierarchy is given in layers, in the sense that subsets in the same layer have the same nesting depth. In [BKK05] hierarchical graph is a system of graphs of various types that are grouped into packages. Hierarchical graphs in [Pa04] are obtained from hypergraphs by adding a parent assigning function to them. Nodes and edges can be assigned as a child of any other node or edge. But in contrast to our approach only the graph is structured, whereas the rules only are given at the topmost level. Hierarchical, Reconfigurable Hierarchical, PetriPetri Reconfigurable Nets 1737 Nets 4 Basics of Reconfigurable Petri Nets In this section we give the basic notions. Note that in ReConNet the underlying type of nets are decorated place/transition nets. To concentrate on the essential notions, in this paper we use place/transition nets, but the corresponding technical report [Pa18] deals explicitly with decorated place/transition nets. Moreover, in [Pa18] the underlying categorical requirements are proven for place/transition nets, decorated place/transition nets, as well as for algebraic high-level nets. We use the algebraic approach to Petri nets, where the pre- and post-domain functions pre, post : T → P ⊕ map the transitions T to a multiset of places P ⊕ given Í by the set of all linear sums over the set P. A marking is given by m ∈ P ⊕ with m = p ∈P k p · p. The Í ≤ operator can be extended to linear sums: For m1, m2 ∈ P ⊕ with m1 = p ∈P k p · p and Í m2 = p ∈P lp · p we have m1 ≤ m2 if and only if k p ≤ lp for all p ∈ P. The operations “+ “ and “– “ can be extended accordingly. Here, we introduce reconfigurable place/transition nets with labels and subtyping of labels for the rules. These labels need a name space that is given by a partial order (A, ≤, g A) with a greatest element, a ≤ g A for all a ∈ A. g A is similar to the common supertype in a type hierarchy. The labelling function is provided with an order for subtyping, this allows more abstract rules that can be applied for occurrences with lesser labels, for an example see Sect.2. Definition 4.1 (Labelled place/transition nets) A (marked labelled place/transition) net is given by N = (P, T, pre, post, pl, tl, M) over the name space A = (AP, AT ) with partial orders (AP, ≤ A, g p ) and (AT , ≤T , gT ). P is a set of places and T is a set of transitions. pre : T → P ⊕ maps a transition to its pre-domain and post : T → P ⊕ maps it to its post-domain. Moreover, pl : P → (AP, ≤ A, g p ) is a label function mapping places to a name space, tl : T → (AT , ≤T , gT ) is a label function mapping transitions to a name space and M ∈ P ⊕ is the marking denoted by a multiset of places. A transition t ∈ T is M-enabled for a marking M ∈ P ⊕ if we have pre(t) ≤ M. The successor marking m 0 is computed by M 0 = M − pre(t) + post(t) and represents the result of a firing step M[t > M 0. Note, we do not require P ∩ T = ∅ since this is not necessary. This condition would require constructing the transformation step explicitly to ensure that the target net M in Fig. 7 satisfies this construction as well. A reconfigurable Petri net RN = (N, R) consists of a Petri net N and a set of rules R. This allows reconfigurable Petri nets to modify themselves. Rules and occurrences are defined by net morphisms. Net morphisms are given as a pair of mappings for the places and the transitions preserving the structure, the labels and the marking. Given two nets N1 and N2 as in Def. 4.1 a net morphism f : N1 → N2 is given by f = ( fP : P1 → P2, fT : T1 → T2 ), so 8174 Jan-Uriel Lorbeer, Lorbeer, Julia Padberg Padberg that pre2 ◦ fT = fP⊕ ◦ pre1 and post2 ◦ fT = fP⊕ ◦ post1 and m1 (p) ≤ m2 ( fP (p)) for all p ∈ P1 . The labels are mapped so that tl2 ◦ fT (t) ≤ tl1 (t) for all t ∈ T1 and pl2 ◦ fp (p) ≤ pl1 (p) for all p ∈ P1 . pre1 / T1 / P1 ⊕ post1 pl1 tl1 v ( (AT , ≤T , gT ) fT fP ⊕ (AP, ≤ P, g P ) h 6 pl2 tl2   pre2 / T2 / P2 ⊕ post2 Moreover, the morphism f is called strict if both fP and fT are injective, if tl2 ◦ fT = tl1 and pl2 ◦ fp = pl1 , and if m1 (p) = m2 ( fP (p)) holds for all p ∈ P1 . Rules r = (L ← K → R) consist of a span of strict net morphisms where L is the left-hand side and K is an interface between L and R the right-hand side. The basic idea is to find L in the net N and replace it by R. Therefore an occurrence morphism o : L → N is required to identify the relevant parts of the left-hand side L in N. Given a rule r and an occurrence o a (r,o) transformation step N ===⇒ M is constructed in two steps by the commutative squares via a gluing construction, that is a pushout. Fig. 7 illustrates the transformation of a net using two pushouts (PO1) and (PO2). An intuitive explanation for a pushout is to take two nets N1, N2 that overlap in some I. Now we glue N1 and N2 together over this common interface I, obtaining a new net N1 +I N2 that is the union of both nets factorized by an equivalence relation induced by the inclusion of I into N1 and N2 . Lo K /R o (PO1) (PO2)    N o D /M Fig. 7: Net transformation Given a rule with an occurrence o : L → N the gluing condition has to be satisfied in order to apply a rule at a given occurrence. Its satisfaction requires that the deletion of a place implies the deletion of the adjacent transitions, and that the deleted place’s marking does not contain more tokens than the corresponding place in L. After finding an occurrence of a left-hand side L in a net, the effect of applying a rule is to remove all obsolete elements and add all fresh elements. The elements of K are preserved, providing us with well-defined attachment points for R. This transformation concepts is based on M-adhesive transformation systems [Eh06] and is given in terms of category theory, so that is allows the application of the concepts and results Hierarchical, Reconfigurable Hierarchical, PetriPetri Reconfigurable Nets 1759 Nets to high-level structures such as graphs, typed attributed graph, hyper-graphs, various types of Petri nets, algebraic signatures and specifications. This is possible because place/transition nets can be proven to be an M-adhesive transformation category [Eh06, Pa15] and nets with labels and subtyping in [Pa18]. Hence these results hold for the corresponding type of Petri net: • Local Church-Rosser Theorem for pairwise analysis of sequential and parallel independence see Thm. 5.12 in [Eh06] • Parallelism Theorem for applying independent rules and transformations in parallel see Thm. 5.18 in [Eh06] • Concurrency Theorem for applying E-related dependent rules simultaneously see Thm. 5.23 in [Eh06] • Embedding and Extension Theorem for transferring transformations and analysis results to more complex scenarios see Thms. 6.14 and 6.16 in [Eh06] • Local Confluence Theorem and Completeness of critical pairs for analysing conflicts and for showing local Confluence see Thm. 6.28 and Lemma 6.22 in [Eh06] 5 Hierarchies of Nets and Rules A hierarchical reconfigurable Petri net uses substitution transitions to implement the hierarchy. A substitution transition is a special kind of transition that itself does not fire, instead it contains a subnet that defines the behaviour that takes place in its stead. Following this basic definition of substitution transitions, different implementations suited for specific purposes are possible, this work focuses on the variant of the substitution transition based hierarchical Petri net that have been presented in [JK09]. Each substitution transition has its own subnet with its own local rules. All places that share an edge with a substitution transition are called the transition’s connecting places. For each connecting place of the substitution transition there exists a corresponding connecting place in the transition’s subnet with the same marking. Via these places tokens enter and leave the subnet. Any transition that may fire belongs either to the main net or to some subnet, but it cannot be a substitution transition. Any net may contain multiple substitution transitions, each instantiating exactly its own subnet. Although multiple substitution transitions may instantiate the same subnet layout, each substitution transition has it’s own permanent instance. This leads to a behaviour of the main nets that relies solely on the firing of the subnets, i.e the firing of the flattened net. 176Lorbeer, 10 Jan-Uriel Lorbeer, Julia Padberg Padberg Fig. 8: Flattening of a substitution transition. Figure 8 shows in the top half a hierarchical net with it’s main net M N and a subnet SN. In the main net the substitution transition st1 has two connecting places: p0 has an edge connecting it to st1 and st1 has an edge connecting it to the place p1. These places can also be found in the subnet as connecting places with edges to and from different transitions. If tokens are added to the place p0 via the transition t1 these also appear in the subnet. There SNs transition sub_t1 can fire and remove tokens from p0 resulting in the removal of the same tokens from p0 in M N. Subnets may contain substitution transitions containing further subnets resulting in a nested hierarchy. Reconfigurable Petri nets use transformation rules to reconfigure themselves. The chosen hierarchical model allows two different rule concepts: global rules and local rules. Hierarchical, Reconfigurable Hierarchical, Petri Reconfigurable Nets Petri Nets177 11 Fig. 9: Application of global rules to a hierarchical Petri net. A global rule is a general rule that may be applied in any net on any level of the whole hierarchical net. So occurrences can be in the main net, its subnets, all their subnets and so forth. Fig. 10: Application of individual rules to a hierarchical Petri net. 178Lorbeer, 12 Jan-Uriel Lorbeer, Julia Padberg Padberg A local rule that is applied to a (sub-)net allows occurrences to be found in that specific net only. Local rules enable the dynamic modification of a specific part of a hierarchical net. The advantage is that rules can be created without knowledge of other parts of the hierarchical net. Local rules are given for one subnet only, whereas global rules belong to the hierarchical net. They can be applied in all subnets since their labels are greater than the labels in the subnet. For details see Subsection 2.2 in [Pa18]. The name space is given by the disjoint union of all local name spaces, so that local rules can be applied only with in the given subnet. Local rules respect the hierarchical net borders so that no transformation may effect more than one (sub-)net. Hence, one restriction is imposed on the rules: Substitution transitions may not be part of a rule. As a consequence connecting places may not be deleted or added by a rule, but they can be part of one. This is due to the gluing condition which requires that places may only be deleted if the adjacent transition is deleted as well and no tokens are left over. Since connection places are neighbours of substitution transitions that cannot occur in a rule, they remain unchanged. Subsequently, we define substitution os transition by subnets formally. Figure 11 shows an example for a very basic substitution rule. Substitution transition are mapped to such rules given by the mapping subst : sT → SR N where SR N is a set of substitution rules. The definition of the reconfigurable hierarchical Petri net requires the substitution transition Fig. 11: An exemplary basic substitution rule. together with its adjacent places, called net Net(t) of a transition t. Definition 5.1 (Net(t)) Given N = (P, T, pre, post, pl, tl) then for a transition t ∈ T the net of t is the net Net(t) = (• t ∪ t •, {t}, pre |t , post |t , pl |• t∪t • , tl | {t } ). With this, reconfigurable hierarchical Petri nets can be formally defined. A reconfigurable hierarchical Petri net consists of a reconfigurable net with substitutions and a set of global rules. They both are defined over a common name spaceA = (AP, AT )The reconfigurable net with substitutions consist of a place/transition net N, a set of local rules R N and a set of substitution rules SR N together with the mapping of substitution transitions to substitution rules subst : sT → SR N . Hierarchical, Reconfigurable Hierarchical, Petri Reconfigurable Nets Petri Nets179 13 Definition 5.2 (Hierarchical reconfigurable Petri net) A hierarchical reconfigurable Petri net HN = (RN, A, GR) is given by its name space A = (AP, AT ), a set of global rules GR over A = (AP, AT ), and a reconfigurable net with substitutions RN = (N, R N , SR N ): 1. N = (P, T, pre, post, pl, tl, M) is a place/transition net over (APN , ATN ) so that, • P is a set of places. • T is a set of transitions. • T contains substitution transitions sT ⊆ T. • pre : T → P ⊕ is a function used for the pre-domain of each transition. • post : T → P ⊕ is a function used for the post-domains of each transition. • − ATN is a naming function for transitions, where substitution transitions tl : T → have their own name space AsT ⊆ ATN so that tl(sT) ⊆ AsT and injective tl |sT . Moreover, regular transitions are not allowed to use that name space. tl(T\sT) ⊆ ATN \AsT . • − APN is a naming function for places, where the set of connecting places pl : P → cP = {•t ∪ t• | t ∈ sT } ⊆ Pis given by the neighbourhood of the substitution transitions and the name space of the connecting places AcP ⊆ APN satisfies pl(cP) ⊆ APN . Moreover, regular places are not allowed to use that name space. tl(P\cP) ⊆ APN \Ac P . • M is a set of tokens withM ∈ P ⊕ . 2. R N is a set of local rules over (APN , ATN \ AsT ). 3. SR N is a set of substitution rules together with a mapping of substitution transitions to substitution rules subst : sT → SR N so that subst(t) = (Net(t) ← − CP(t) → − SN t ) with • the interface CP(t) = (• t ∪ t •, ∅, ∅, ∅, pl |• t∪t • , ∅) consisting of connecting places only. • a reconfigurable net with substitutions SN t = (RN t , R t , SRt ) over At = (AtP, ATt ) with Ac P ⊆ AtP . Chapter 5 in [JK09] states that the flattening of a hierarchical net that uses substitution transitions must remove each substitution transition and insert its subnet into the supernet by fusing the connecting places. This process corresponds to applying the substitution rules from Def. 5.2. Only one substitution for each substitution transition is applicable to RN. Corollary 5.3 (Set of substitutions S N ) Given a reconfigurable net with substitutions RN = (N, R N , SR N ). For every substitution transition t ∈ sT and its substitution rule sr = subst(t) there exists exactly one injective occurrence o of sr. These substitutions are 180Lorbeer, 14 Jan-Uriel Lorbeer, Julia Padberg Padberg collected in a set of substitutions S N = {(sr, o) | sr = subst(t) and injective o : Net(t) ,→ RN }. Due to the global and local rules, flattening construction is more complex than for a normal hierarchical Petri net. Flattening of a normal hierarchical Petri net looses all information of the hierarchical borders, but this information is needed for the correct application of local and global rules in the flattened net. Hence, we use the disjoint union of the subnet’s name spaces. First we investigate the parallel independence [Eh06] of the substitution rules. If any two s1, s2 ∈ S with s1 , s2 are pairwise parallel independent the Parallelism Theorem states that they are also sequentially independent [Eh06]. All substitution rules sr together with their occurrences are independent from each other if any two sr1, sr2 with sr1 , sr2 are pairwise independent. So the proof of parallel independence of two arbitrary substitutions s1, s2 ∈ S is sufficient to prove Lemma 5.4. Lemma 5.4 (Pairwise Independence of Substitutions) Given a reconfigurable net with substitutions RN = (N, R N , SR N ). Any two substitutions s1, s2 ∈ S N with s1 , s2 are pair-wise independent. Proof: We show for two arbitrary substitutions s1 , s2 the set theoretic representation of parallel independence o1 (ST1 ) ∩ o2 (ST2 ) ⊆ o1 (l1 (CP1 )) ∩ o2 (l2 (CP2 )) holds. SN t1 o r1 CP(t1 ) l1 / Net(t1 ) Net(t2 ) o r2 CP(t2 ) l2 / SN t2 n1 k1 g2 o1 o2 g1 k2 n2   u " | )   H1 o r10 D1 l10 /Go r20 D2 l20 / H2 The left-hand side of any rule r s of (r s, o) ∈ S N contains by Def. 5.2 only a net Net(t). As specified in Def. 5.1 Net(t) contains only a substitution transition t and t’s pre- and post-domains. The interface CP(t) contains only t’s pre- and post-domains. Considering two substitutions s1, s2 ∈ S N with s1 , s2 , the intersection between their occurrences only considering transitions must be empty because otherwise t1 = t2 and thus s1 = s2. Since CP(t1 ) only contains places and since Net(t1 ) contains one distinct transition t1 and Net(t2 ) the another one t2 , it follows: o1T (Net(t1 )) ∩ o2T (Net(t2 )) = ∅ ⊆ ∅ = o1T (l1 (CP(t1 ))) ∩ o2T (l2 (CP(t2 ))) Now we consider the places. Let p ∈ o1P (Net(t1 )) ∩ o2P (Net(t2 )). Hence p ∈ (• t1 ∪ t1• ) ∩ (• t2 ∪ t2• ) that is p ∈ CP(t1 ) ∩ CP(t2 ) by definition of CP. Since l1, l2, o1P and o2P are functions we conclude that p ∈ (l1 (CP(t1 ))) ∩ (l2 (CP(t2 ))) and p ∈ o1P (l1 (CP(t1 ))) ∩ o2P (l2 (CP(t2 ))). Thus: o1P (Net(t1 )) ∩ o2P (Net(t2 )) ⊆ o1P (l1 (CP(t1 ))) ∩ o2P (l2 (CP(t2 ))) which proves any two s1, s2 ∈ S with s1 , s2 are pairwise parallel independent.  Hierarchical, Reconfigurable Hierarchical, Petri Reconfigurable Nets Petri Nets181 15 Theorem 5.5 is proven using Lemma 5.4. Theorem 5.5 (F L AT(N, SR N ) Flattening of reconfigurable net with substitutions) Given a reconfigurable net with substitutions (N, SR N ) any possible transformation sequence SN of rules S N yields the same (up to isomorphism) well-defined net N ==⇒ F L AT(N, SR N ). Proof: With all s ∈ S N being mutually independent, [Eh06] states all the transformationÍsequences ∗ s∈S N s HN ⇒ = F are equivalent and there exists a parallel transformation sequence HN =======⇒ F. Let F L AT(N, SR N ) := F. Such a parallel transformation sequence can always be constructed and is unique up to isomorphism.  The flattening of a hierarchical reconfigurable Petri net to a reconfigurable net needs to include global as well as local rules and is given recursively based on flattening of nets with substitution. Definition 5.6 (Flattening) The flattening is defined for a hierarchical net HN = (RN, A, GR) given by a reconfigurable net RN = (N, R N , SR N ), a name space A = (AP, AT ) and a set of global rules GR as given in Def. 5.2 recursively by: 1. Given RN = (N, R N , SR N ) over A = (APN , ATN ) with substitution transitions sT = ∅ we have: f lat(RN) = (N, R N ) over A 2. Given RN = (N, R N , SR N ) over A = (APN , ATN ) with substitution transitions sT , ∅ we have: Ò f lat(RN) = f lat(F L AT(N, SR N ), R, SR) over A with • A = t ∈sT (AP \ Acp ) ] Ac P t Ò • R = ( t ∈sT R t ) ] R N Ò • SR = ( t ∈sT SRt 3. f lat(HN) = (NFlat , GR ∪ R Flat ) over A with f lat(RN) = (NFlat , R Flat ) where the name space A is the union of the name spaces, so that the global labels are greater than the corresponding local labels (see [Pa18]). Definition 5.7 (Well-defined hierarchical reconfigurable Petri net) A hierarchical re- configurable Petri net HN = (RN, A, GR) is well-defined if and only if the f lat(HN) is well-defined. 182Lorbeer, 16 Jan-Uriel Lorbeer, Julia Padberg Padberg 6 Hierarchies in ReConNet During the simulation ReConNet’s simulation engine uses the flat representation of a hierarchical reconfigurable Petri net for transition firing and rule application, because this allows using ReConNet’s simulation engine to handle the hierarchical net, i.e its flattened net. However, for the user this remains transparent and the visual interface continues presenting the hierarchical view. While transitions are fired and transformations are made on the flat net the hierarchical view visualizes the changes accordingly. While developing the nets and transformation rules, the hierarchy is established and the simulation requires the flattened net that is the result of the flattening construction. The application of local rules in the flat net needs one single name space for places and transitions A = (APN , ATN ). This name space needs to include all of the disjoint name spaces of the (sub-)nets. This single name space is created during the flattening. Whenever a subnet is inserted into its supernet all places and transitions that are not connecting places get a prefix to their names that is unique to the substitution transition that was replaced. This way the naming preserves hierarchy borders and (sub-)net identities and so the names of places and transitions are specific enough that a rule meant for only a specific (sub-)net can be limited to the correct part of the flat net. For persistence of a hierarchical reconfigurable Petri net from ReConNet the hierarchical reconfigurable Petri net’s flat net and the substitution rules. The hierarchical reconfigurable Petri net is saved as a tuple of the main net, as a reconfigurable Petri net, its substitution rules and the flat net, so that HN = hRN, SR, Flat(RN, SR)i. So, the flat net can be loaded directly and needs not to be computed each time again. R! In a transformation unit N1 ==⇒ N2 [KKR08] the as-long-as-possible operator ! forces the rule set R to be applied as long as possible. Since ReConNet is provided with transformation units [Ho16] the flattening construction can be realized using this as-long- SN ! as-possible operator !. In the transformation unit RN ===⇒ F an applicable substitution rule s with an injective occurrence is randomly picked and applied. This step is repeated until all s ∈ S N have been applied, since each s has by construction only one occurrence. Lemma 6.1 (Flattening based on the as-long-as-possible operator ! ) Given a reconfig- sr! urable net with substitutions (N, SR N ) the result F of (N, SR N ) ==⇒ F is well-defined up to isomorphism and isomorphic to F L AT(N, SR N ). Proof: Given the set of substitutions S n based on (N, SR N ) as in Cor. 5.3, any two substitutions s1, s2 ∈ S N are pairwise independent, then the fact that F is well-defined up to isomorphism is proven indirectly: SN ! SN ! If F is not well-defined the transformation sequences (N, SR N ) ===⇒ F and (N, SR N ) ===⇒ Hierarchical, Reconfigurable Hierarchical, Petri Reconfigurable Nets Petri Nets183 17 b exists so that F  F. F b So, there has to exist some M in diagram (1) with ∗ sj ∗ si ∗ ∗ = M =⇒ M j and RN ⇒ RN ⇒ = M =⇒ Mi so that there is neither Mi ⇒ = F nor M j ⇒ = F: Mj Mj :B :B sj sj q∗ ri s ∗ $ ∗ % ∗ RN +3 M (1) :B F RN +3 M (2) M +3 F 9A i j / . si ∗ si sj $ $ Mi Mi sr! For RN ==⇒ F and RN ==⇒ F sr! b both substitutions si and s j have to be applied. All s ∈ S are pairwise sequential independent, so any sequence can be applied in arbitrary order yielding the same well-defined resulting net [Eh06]. Hence, we obtain diagram (2). Any two s ∈ S are pairwise parallel independent, so are si and s j , thus their sequence is interchangeable si is always applicable to M j and s j is always applicable to Mi both always leading to the same net Mi j . So F  F b for HN ==sr! ⇒ F and HN ==⇒ F sr! b and thus F is well-defined up to isomorphism.  Since all s ∈ S are independent from another, each s ∈ S N of the sr! transformation RN ==⇒ Fb Í s∈S s can be applied exactly once for each of its occurrences. RN =====⇒ F can equivalently be ∗ b s1 sn applied as a transformation sequence RN ⇒ = F = RN =⇒ ... ==⇒ F. So to prove that F  F requires to show that no s can be applied more than once. Theorem 6.2 (Equivalence of Flattening Constructions) Given a reconfigurable net with substitutions (N, SR N ). The transformation using the as-long-as-possible opera- tor ! Í is equivalent to the flattening construction in Thm. 5.5: s∈S N s SN ! RN =======⇒ F L AT(N, SR N ) and RN ===⇒ F implies F L AT(N, SR N )  F. Proof: For any s ∈ S to be able to be applied more than once it would have to be independent from itself. s1 = s2 implies they contain the same substitution transition t1 = t2 , it follows: (o1T (net(t1 )) ∩ o2T (net(t2 )) , ∅) * ∅ = o1T (l1 (CP1 )) ∩ o2T (l2 (CP2 )). Thus s1 and s2 are not independent. Hence any s is not independent from itself and thus can only be applied once.  7 Conclusion This paper introduces substitution transitions for hierarchical reconfigurable Petri nets. The main contribution is a formal definition of hierarchical reconfigurable Petri nets and its flattening construction. 184Lorbeer, 18 Jan-Uriel Lorbeer, Julia Padberg Padberg This work presents a first step to the integration of reconfigurable hierarchical Petri nets into the ReConNet tool [Pa12, Re17]. Ongoing work will accomplish support of hierarchical Petri nets in ReConNet. First a hierarchy needs to be introduced into ReConNet to allow transformation simulation, including an appropriate update to ReConNet’s persistence module to allow proper storing and restoring of hierarchical nets. Then individual rules will be added to allow the functionality of a reconfigurable net. For net verification and validation purposes the flat representation of the hierarchical reconfigurable Petri net will be used. References [Ak17] Akshay, S.; Chakraborty, Supratik; Das, Ankush; Jagannath, Vishal; Sandeep, Sai: On Petri Nets with Hierarchical Special Arcs. In: 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany. pp. 40:1–40:17, 2017. [BH01] Busatto, Giorgio; Hoffmann, Berthold: Comparing Notions of Hierarchical Graph Trans- formation. Electr. Notes Theor. Comput. Sci., 50(3):310–317, 2001. [BKK05] Busatto, Giorgio; Kreowski, Hans-Jörg; Kuske, Sabine: Abstract hierarchical graph transformation. Mathematical Structures in Computer Science, 15(4):773–819, 2005. [Bo06] Bottoni, Paolo; Rosa, Fabio De; Hoffmann, Kathrin; Mecella, Massimo: Applying Algebraic Approaches for Modeling Workflows and their Transformations in Mobile Networks. Mobile Information Systems, 2(1):51–76, 2006. [Br14] Bruni, Roberto; Montanari, Ugo; Plotkin, Gordon D.; Terreni, Daniele: On Hierarchical Graphs: Reconciling Bigraphs, Gs-monoidal Theories and Gs-graphs. Fundam. Inform., 134(3-4):287–317, 2014. [CP17] CPN-Tools. http://http://cpntools.org/, 2017. Last accessed: 2017-11-01. [DHP02] Drewes, Frank; Hoffmann, Berthold; Plump, Detlef: Hierarchical Graph Transformation. J. Comput. Syst. Sci., 64(2):249–283, 2002. [Eh06] Ehrig, H.artmut; Ehrig, Karsten; Prange, Ulrike; Taentzer, Gabriele: Fundamentals of Algebraic Graph Transformation. EATCS Monographs in TCS. Springer, 2006. [GE12] Gabriel, Karsten; Ehrig, Hartmut: Modelling of Communication Platforms Using Algebraic High-Level Nets and Their Processes. In (Heisel, Maritta, ed.): Software Service and Application Engineering: Essays Dedicated to Bernd Krämer on the Occasion of His 65th Birthday. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 10–25, 2012. [GNH12] Gottmann, Susann; Nachtigall, Nico; Hoffmann, Kathrin: On Modelling Communication in Ubiquitous Computing Systems using Algebraic Higher Order Nets. ECEASST, 51, 2012. [He12] Heiner, Monika; Herajy, Mostafa; Liu, Fei; Rohr, Christian; Schwarick, Martin: Snoopy–a unifying Petri net tool. In: International Conference on Application and Theory of Petri Nets and Concurrency. Springer, pp. 398–407, 2012. Hierarchical, Reconfigurable Hierarchical, Petri Reconfigurable Nets Petri Nets185 19 [HEP08] Hoffmann, Kathrin; Ehrig, Hartmut; Padberg, Julia: Flexible Modeling of Emergency Scenarios using Reconfigurable Systems. ECEASST, 12, 2008. [Hi17] HiPS : Hierarchical Petri net Simulator. https://sourceforge.net/projects/hips- tools/, 2017. Last accessed:2017.03.22. [HJS91] Huber, Peter; Jensen, Kurt; Shapiro, Robert M.: Hierarchies in coloured Petri nets. In (Rozenberg, Grzegorz, ed.): Advances in Petri Nets 1990. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 313–341, 1991. [Ho16] Hoff, Christian: Transformationseinheiten als Kontrollstruktur für rekonfigurierbare Petrinetze in ReConNet. Master’s thesis, University of Applied Sciences Hamburg, 2016. [HW18] Harie, Yojiro; Wasaki, Katsumi: A Petri Net Design and Verification Platform Based on The Scalable and Parallel Architecture: HiPS. In: Information Technology-New Generations, pp. 265–273. Springer, 2018. [JK09] Jensen, Kurt; Kristensen, Lars M: Coloured Petri nets: modelling and validation of concurrent systems. Springer, 2009. [JR91] Jensen, Kurt; Rosenberg, Gregorz: High-Level Petri nets: Theory and Application. 1991. Springer, 1991. [KBD16] Kahloul, Laid; Bourekkache, Samir; Djouani, Karim: Designing reconfigurable manufac- turing systems using reconfigurable object Petri nets. Int. Journal of Computer Integrated Manufacturing, pp. 1–18, 2016. [KH10] Köhler-Bußmeier, Michael; Heitmann, Frank: Safeness for Object Nets. Fundam. Inform., 101(1-2):29–43, 2010. [KH11] Köhler-Bußmeier, Michael; Heitmann, Frank: Liveness of Safe Object Nets. Fundam. Inform., 112(1):73–87, 2011. [KKR08] Kreowski, Hans-Jorg; Kuske, Sabine; Rozenberg, Grzegorz: Graph Transformation Units– An Overview. Lecture Notes in Computer Science, 5065:57–75, 2008. [La01] Lakos, Charles: Object Oriented Modeling with Object Petri Nets. In (Agha, Gul; de Cindio, Fiorella; Rozenberg, Grzegorz, eds): Concurrent Object-Oriented Programming and Petri Nets, Advances in Petri Nets. Lecture Notes in Computer Science. Springer, pp. 1–37, 2001. [LO04] Llorens, Marisa; Oliver, Javier: Structural and Dynamic Changes in Concurrent Systems: Reconfigurable Petri Nets. IEEE Trans. Computers, 53(9):1147–1158, 2004. [MGH10] Modica, Tony; Gabriel, Karsten; Hoffmann, Kathrin: Formalization of Petri Nets with Individual Tokens as Basis for DPO Net Transformations. ECEASST, 40, 2010. [MK05] Miyamoto, Toshiyuki; Kumagai, Sadatoshi: A survey of object-oriented Petri nets and analysis methods. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, 88(11):2964–2971, 2005. [Pa04] Palacz, Wojciech: Algebraic hierarchical graph transformation. J. Comput. Syst. Sci., 68(3):497–520, 2004. 186Lorbeer, 20 Jan-Uriel Lorbeer, Julia Padberg Padberg [Pa07] Padberg, Julia; Hoffmann, Kathrin; Ehrig, Hartmut; Modica, Tony; Biermann, Enrico; Ermel, Claudia: Maintaining Consistency in Layered Architectures of Mobile Ad-Hoc Networks. In (Dwyer, Matthew B.; Lopes, Antónia, eds): Fundamental Approaches to Software Engineering 2007. volume 4422 of Lecture Notes in Computer Science. Springer, pp. 383–397, 2007. [Pa12] Padberg, Julia; Ede, Marvin; Oelker, Gerhard; Hoffmann, Kathrin: ReConNet: A Tool for Modeling and Simulating with Reconfigurable Place/Transition Nets. ECEASST, 54, 2012. [Pa15] Padberg, Julia: Reconfigurable Petri Nets with Transition Priorities and Inhibitor Arcs. In (Parisi-Presicce, Francesco; Westfechtel, Bernhard, eds): Graph Transformation - 8th Int. Conf. volume 9151 of Lecture Notes in Computer Science. Springer, pp. 104–120, 2015. [Pa18] Padberg, Julia: Subtyping for Hierarchical, Reconfigurable Petri Nets. ArXiv e-prints, 2018. [PK18] Padberg, Julia; Kahloul, Laid: Overview of Reconfigurable Petri Nets. In: Festschrift in Memory of Hartmut Ehrig. Springer, 2018. accepted. [Ra03] Ratzer, Anne Vinter; Wells, Lisa; Lassen, Henry Michael; Laursen, Mads; Qvortrup, Jacob Frank; Stissing, Martin Stig; Westergaard, Michael; Christensen, Søren; Jensen, Kurt: CPN tools for editing, simulating, and analysing coloured Petri nets. In: International Conference on Application and Theory of Petri Nets. Springer, pp. 450–462, 2003. [Re17] ReConNet. https://reconnetblog.wordpress.com/, 2017. Last accessed: 2017.05.16. [Tâ12] Târnauca, Bogdan; Puiu, Dan; Comnac, Vasile; Suciu, Constantin: Modelling a flexible manufacturing system using reconfigurable finite capacity Petri nets. In: 13th Int. Conf. on Optimization of Electrical and Electronic Equipment. pp. 1079–1084, May 2012. [Va98] Valk, Rüdiger: Petri Nets as Token Objects: An Introduction to Elementary Object Nets. In (Desel, Jörg; Suárez, Manuel Silva, eds): Application and Theory of Petri Nets 1998, 19th International Conference, ICATPN ’98, Lisbon, Portugal, June 22-26, 1998, Proceedings. volume 1420 of Lecture Notes in Computer Science. Springer, pp. 1–25, 1998. [Va04] Valk, Rüdiger: Object Petri nets. In: Lectures on Concurrency and Petri Nets, pp. 819–848. Springer, 2004.