Invariant Calculations for P/T-Nets with Synchronous Channels⋆ Simon Bott1 , Daniel Moldt1 , Laif-Oke Clasen1 and Marcel Hansson1 1 University of Hamburg, Faculty of Mathematics, Informatics and Natural Sciences, Department of Informatics http:// www.paose.de Abstract Partitioning of systems generally leads to simpler system models and reduced cost in subsequent computations. The control structure of such a system can be covered by P/T-nets. Enhancing them with synchronous channels allows for decoupling net modules via a kind of interface. In this paper, we discuss how to extend former definitions of Place/Transition nets with synchronous chan- nels and modular structure by general synchronization. Concerning modeling capabilities in terms of expressiv- ity, the usage of synchronous channels introduces a more powerful modeling technique than traditional P/T-nets. Introducing new concepts requires discussing how traditional verification means are kept in the new formalism. The main contributions of this paper are the extensions of the existing definitions of P/T nets with syn- chronous channels and inducing modular structures on the net templates. In addition, existing approaches of verification options regarding invariant computation are applied to our definitions of the model. When modeling the control structures of a system using P/T nets with synchronous channels, the modules of the system can be covered with invariants by inducing a specific structure of the net modules. Restricting the possible interconnections of net modules can support verification with invariants. Keywords P/T-nets, Synchronous Channels, Structuring Mechanisms, Petri Net Modules, Modeling, Invariants, Reference Nets, Renew 1. Introduction Petri nets and specifically P/T-nets (Place/Transition-nets) have proven themselves to be useful for modeling complex concurrent systems and to allow formal verification of properties. Invariants, as one well-known property, support the verification of various properties of such systems, for example, liveness and boundedness. There are a variety of algorithms used for computing invariants that differ in their computational demands, resulting from different constraints desired for the resulting invariants. They range from methods based on Gaussian elimination [1] for computing any kind of basis of invariants to linear programming methods that compute minimal positive invariants [2, 3]. Another strategy for calculating invariants is the decomposition of systems, as in [4]. Here, a large system is decomposed into smaller subsystems and the corresponding calculations of invariants are carried out in the smaller subsystems. The complexity resulting from modeling large systems makes the verification of such models compu- tationally hard. It is the modular approach to modeling we want to consider in this paper. The division of large systems into smaller subsystems, or modules, reduces complexity by allowing individual modules to be examined independently of one another. However, the interactions between modules still have to be considered. The model used in this paper is P/T nets with synchronous channels [5], whereby the definitions are refined within this paper. These are ordinary P/T nets that can communicate with each other via synchronous channels, similar to those of Christensen and Hansen [6, 7], which support synchronization of transitions. PNSE’24: International Workshop on Petri Nets and Software Engineering, June 24–25, 2024, Geneva, Switzerland ⋆ Supported by several colleagues and students. © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings 104 Simon Bott et al. CEUR Workshop Proceedings 104–121 The main question in this paper is how existing verification options and the modular approach of P/T nets with synchronous channels can be combined. The hypothesis is that decomposition based on the modular approach allows invariants within the subsystems to be calculated independently of each other, which means that these calculations can be distributed. The purpose of introducing such a concept covers more efficient verification in our tool and a structured / an object-oriented way of modeling by enhanced encapsulation via interfaces (modeled as synchronous channels. In [8] and [9], some simple versions of invariant calculations have been introduced to Renew. The Ptc-nets (Place/Transition nets with Channels) are used and extended here in a simple manner. Additionally it is shown in [5] that Ptc-nets can be unfolded to P/T-nets and thus can model the same class of Petri net models as ordinary P/T-nets, however, in a more compact and structured way. In this paper, we present a variant of this and the modular nets of [10] and the Renew-based version in [5], we illustrate how P-invariants can be computed due to modularization, and we discuss the application of this modularized modeling to software modules. Our Petri nets-, Agent- and Organization-based Software Engineering approach (Paose, [11]) uses a special form of nets to model the communication of system components / agents. The Ptc-net variant introduced here can be used to support such system models. The structure of the paper is the following: We first recall the definitions of P/T-nets and the equation from which invariants are derived in Section 3. Then we present our modular model in Section 4 informally with an example and with a formal definition, concluding in constructing an equivalent P/T-net. This leads to the examination of invariants in Ptc-system nets in Section 5, where we construct the incidence matrix by choosing a favorable ordering of its rows and columns and cover approaches to P- and T-invariants. In Section 6, we briefly show how invariants in Ptc-system nets can be used to verify some of their properties. Whereupon another example is explained in Section 7. In Section 8, we reflect on our findings and discuss further ideas concerning the application of the provided results. Finalized by the conclusion in Section 9. 2. Related Works A common approach to limiting complexity is to identify and condense parts of nets that are similar in form and function. Higher-level nets like colored Petri nets serve such a purpose [12, 13]. colored Petri nets are extended upon to support synchronization through colored communication channels in [7]. Further, the formal definition of place invariants is extended to colored Petri nets with and without channels. In this paper, the modular approaches to reducing the complexity of analysis are of particular interest. In [10], modular P/T-nets are introduced, in which ordinary P/T-nets act as modules, and so-called place fusion sets and transition fusion sets define the possible interactions between modules. They allow the sharing of places and the synchronization of transitions, respectively. The resulting P-invariants and state spaces of modular P/T-nets are examined. The state space construction of modular P/T-nets is expanded upon in [14] to also include shared places. The possibility of designing an algorithm that incorporates place fusions directly is investigated. However, such an algorithm would have similar results as those obtained by first transforming place fusions into transition fusions. Consequently, possible schemes for such transformations are analyzed. In [15, 16], the modular approach is extended to colored Petri nets with the introduction of modular CP-nets. In comparison to modular P/T-nets, they contain colored Petri nets instead of P/T-nets as modules, with place fusion sets and transition fusion sets continuing to control interactions between modules. The resulting P-invariants and state spaces of modular CP-nets are examined. In [5] P/T-nets with synchronous channels and modular PTC-nets are introduced. A formal definition and implementation in Renew are given for both models. The models are, however, limited in that only two transitions can be synchronized at a time. Further, verification is done by first constructing equivalent P/T-nets. With HERAKLIT a new modular approached was introduced in [17] based on the composition 105 Simon Bott et al. CEUR Workshop Proceedings 104–121 calculus and interface nets by Wolfgang Reisig [18]. In HERAKLIT each module is a net with two interfaces, which can contain places and transitions. A whole system is then composed by merging the same labeled elements of the interfaces of the modules. Merging two transitions this way is in some regards similar to connecting them via synchronous channels as the two transition are merged into one transition while with channels they behave as one transition. The looser coupling with channels allows a more dynamic behavior though as a transition could participate in different synchronizations. Aside from Petri nets, modular approaches also exist for other models of describing concurrent processes. One example is the use of communicating sequential processes [19] in solving distributed constraint satisfaction problems [20]. Modeling complex systems strives to partition systems into smaller parts. The coupling of those parts should be loose compared to the internal coherent components. The Paose approach to model the control structure of systems via Petri nets with a clear interface supports this directly. Mapping objects, agents, services, etc. to net modules is a straightforward approach. Modeling the communication between them via synchronous channels and P/T-nets allows for the reduction of the modeling to the orchestration and choreography of such system components. Encapsulation and abstraction of parts of the system by separating the channels is straightforward. The Paose approach can incorporate this verification approach directly as our agents follow the design to communicate as specified by the corresponding Agent interaction protocol diagrams (Aips). Aips extend the UML sequence diagrams[21] by additional alternatives and concurrency. [11] Additionally, a formal semantics for Aips based on Petri nets was proposed in [22]. As discussed above these can be restricted to our Ptc-net definitions for verification purposes. Currently, we are experimenting with the application to our Heraklit Agents [23]. These Heraklit Agents combine Reference Nets, Agents and HERAKLIT Modules [17]. 3. Foundations and Problem Formulation We start by defining P/T-nets and their invariants. Definition 1. A P/T-net is a tuple 𝑁 = (𝑃, 𝑇, 𝐹, 𝑊, 𝑚0 ), where: • 𝑃 is a finite set of places • 𝑇 is a finite set of transitions, 𝑃 and 𝑇 are disjoint: 𝑃 ∩ 𝑇 = ∅ • 𝐹 ⊆ (𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ) is a set of directed arcs • 𝑊 : 𝐹 → N+ is the arc weight function • 𝑚0 : 𝑃 → N0 is the initial marking It is helpful to extend the arc weight function in the following way: Definition 2. The extended arc weight function 𝑊 ̃︁ : (𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ) → N0 returns 0 for places/- transitions that share no directed arc: {︂ 𝑊 (𝑥, 𝑦), if (𝑥, 𝑦) ∈ 𝐹 𝑊 (𝑥, 𝑦) = ̃︁ (1) 0, otherwise Now we define the enabling and firing rules of a P/T-net. 𝑡 Definition 3. A transition 𝑡 is enabled for a marking 𝑚, denoted by 𝑚 →, iff ∀𝑝 ∈ 𝑃 : 𝑊 ̃︁ (𝑝, 𝑡) ≤ 𝑚(𝑝) (2) Definition 4. The successor marking 𝑚′ (𝑝) after firing a transition 𝑡 from a marking 𝑚, denoted by 𝑡 𝑚 → 𝑚′ , is defined as ∀𝑝 ∈ 𝑃 : 𝑚′ (𝑝) = 𝑚(𝑝) − 𝑊 ̃︁ (𝑝, 𝑡) + 𝑊 ̃︁ (𝑡, 𝑝) (3) 106 Simon Bott et al. CEUR Workshop Proceedings 104–121 At this point, we give another interchangeable definition of a P/T-net that consists of the backward incidence matrix pre, describing the input of transitions, and the forward incidence matrix post, describing the output of transitions[24]. It is going to be useful when constructing a P/T-net from our Ptc-net. Definition 5. A P/T-net is a tuple 𝑁 = (𝑃, 𝑇, pre, post, 𝑚0 ), where: • 𝑃 is a finite set of places • 𝑇 is a finite set of transitions, both sets are disjoint: 𝑃 ∩ 𝑇 = ∅ |𝑃 |×|𝑇 | • pre, post ∈ N0 are the backward and forward incidence matrix respectively. The relation between this definition and Definition 1 is illustrated by expressing the elements of pre, post through the extended arc weight function: pre𝑝𝑡 = 𝑊 ̃︁ (𝑝, 𝑡) (4) post𝑝𝑡 = 𝑊 ̃︁ (𝑡, 𝑝) (5) The effect of a single transition is the net change that results from its firing. The effects of all transitions of a given net are aggregated in the incidence matrix. It is central to the study of a net’s structural properties, such as invariants. Definition 6. The incidence matrix Δ ∈ Z|𝑃 |×|𝑇 | of a P/T-net 𝑁 is defined as: Δ = post − pre (6) |𝑇 | Now we can express the change of net markings in the form of an equation, where 𝑥 ∈ N0 contains the firing counts of each transition and 𝑚 is the resulting marking. 𝑚 = 𝑚0 + Δ𝑥 (7) T-invariants describe the special case when the net effect of a composition of firing counts is zero, or more specifically, the zero vector 0. P-invariants describe a weight function for the places of a net that is invariant with regard to the changes in markings resulting from firing transitions. Both can be expressed as solutions of a homogeneous system of equations: Δ𝑥 = 0 (8) ΔT 𝑦 = 0 (9) |𝑇 | Where the non-trivial solutions 𝑥 ∈ N0 ∖ {0} are T-invariants and the non-trivial solutions of 𝑦 ∈ Z|𝑃 | ∖ {0} are P-invariants. It is also common to only consider positive solutions for P-invariants. We conclude with the definition of a multiset and the relevant notations used in this paper. Note that we shorten multisets to their functional components for brevity. A comprehensive overview of multisets can be found in [25]. Definition 7. A multiset 𝑏𝑔 over a set 𝐷 is a function 𝑏𝑔 : 𝐷 → N0 . To differentiate a multiset from an ordinary set, we use a subscript 𝑏, for example, {𝑎, 𝑏, 𝑏}𝑏 . Definition 8. Let 𝑏𝑔1 and 𝑏𝑔2 be two multisets over the same set 𝐷, then their sum 𝑏𝑔3 , denoted by 𝑏𝑔3 = 𝑏𝑔1 ⊎ 𝑏𝑔2 , is defined as: ∀𝑑 ∈ 𝐷 : 𝑏𝑔3 (𝑑) = 𝑏𝑔1 (𝑑) + 𝑏𝑔2 (𝑑) (10) Definition 9. Let 𝐷 be a set, then we denote the set of all multisets over 𝐷 as 𝐵𝑎𝑔(𝐷). 107 Simon Bott et al. CEUR Workshop Proceedings 104–121 Another type of net that will be referred to throughout the paper are reference nets which we will only describe with an informal description. Reference nets introduced in [26] are high-level Petri nets with arbitrary (Java) objects as tokens, that can be modeled and simulated with the tool Renew (The Reference Net Workshop) [27]. In particular, the tokens can be references to other net instances. The communication between net instances is done by synchronous channels (see [6, 7]). Synchronous channels allow for synchronization of transitions. Transitions are equipped with channels and can communicate with other transitions with which they share a channel. Channels are primarily differentiated by their channel identifier. Additionally, channels are assigned a type, for example, downlink and uplink, so that transitions can only communicate with transitions with the same channel identifier of the opposite type. Lastly, parameters allow channels to specify a binding for potential variables that are weights of edges of communicating transitions [26]. 4. Ptc-System Net In the following we repeat the example and parts of the definition given in [5], where some different versions and extensions of [10] were given. 4.1. Informal Introduction We now introduce Ptc-system nets using a simple producer/consumer example with a shared storage (Figure 1) constructed in Renew. Both producer and consumer have an internal logic that determines when they are able to produce or consume. For our example, we reduced them to the simple form where they are either ready or unready. The storage has a capacity and allows storing and retrieving as possible actions. The system net governs the interactions between modules. Both the Consumer and Producer consist of a simple cycle. The transitions tc0 and tp0 are internal transitions and behave normally. The transitions tc1 and tp1, however, are external, discernible from their inscriptions, which denote synchronous channels in Renew. They can’t fire independently; instead, their behavior is controlled by the SystemNet. The Storage consists of a place representing the content it is holding and its complementary place representing its available storage capacity. ts0 allows storing things in the storage, while ts1 allows retrieving things from the storage. Both are external transitions. Additionally, they contain variables that determine the amount transferred and are assigned indirectly by the SystemNet. The SystemNet seems more complex than it really is due to its implementation in Renew. While the reference nets in Renew are more expressive than P/T-nets, we only use them in a restricted form. t0 creates net instances of our modules and stores them in the place NetReferences. t1 acts as an aid to address the individual modules. The key components of the SystemNet are the transitions t2 and t3. They allow the synchronization between the external transitions of multiple modules. t2 synchronizes tp1 and ts0 and binds the variable 𝑥 to the value declared in the inscription of tp1. t3 synchronizes tc1 and ts1 and binds the variable 𝑥 to the value declared in the inscription of tc1. Both t2 and t3 represent synchronization rules governed by the Ptc-system net. (It should be pointed out that, while the binding of variables is done implicitly in Renew through parameters and unification, it is done explicitly in the proper formal definition of the Ptc-system net.) We now go into the key differences in comparison to the modular PT-net presented in [10]. 4.1.1. No shared places To motivate the removal of shared places, we consider the concept of data encapsulation. It is desirable, for example, in object-oriented programming, to limit direct access to the fields/data of an object/module [28]. In P/T-nets these correspond to its passive elements, its places. Furthermore, the synchronization of transitions alone is sufficient because they can emulate shared places. Instead of giving direct access to its places, a module can instead provide transitions that 108 Simon Bott et al. CEUR Workshop Proceedings 104–121 (a) Producer (b) Consumer (c) Storage (d) SystemNet Figure 1: Producer and Consumer synchronization via a shared Storage; see [5] conceptually act as getters/setters. In our example, the shared storage implements this idea. It provides places that are essentially shared, but does so through the sole use of synchronized transitions. This transformation from shared places to synchronized transitions, however, is in general not obvious as shared places can be replaced in different ways. Such transformation schemes are studied in [14], with the best results in regard to modular state space construction being achieved when considering cohesion and coupling between modules. Finally, we gain nice properties for P-invariants, already established in Theorem 6.4 of [10] and further explored in Section 5. 4.1.2. Transitions participating in the same synchronization multiple times Since the transition fusion sets in [10] are sets and not multisets, a given transition can only participate once. Allowing transitions to participate any number of times is a straightforward generalization. This would be useful when an action of one module should be synchronized with the multiple 109 Simon Bott et al. CEUR Workshop Proceedings 104–121 equivalent actions of other modules. If, for example, in our producer-consumer framework, a production process produces multiple goods at the same time, multiple store tasks, symbolized by synchronization with a store transition, would be necessary. From the view of the producer, it would be extraneous which modules in particular fulfill the store tasks. Especially whether it’s synchronizing with multiple different storages or whether one single storage fulfills all store tasks. 4.1.3. Synchronized channels The identification of similar behavior and its appropriate treatment is essential to limiting complex- ity. By assigning transitions that execute interchangeable actions the same channel, many different synchronizations can be established by a single synchronization rule. If, for example, we had two storages, the action of storing something provided by the individual storages would be considered interchangeable from an external view. The producer wouldn’t care which storage responds to its communicated production. Therefore, if we wanted to add more modules representing producers or consumers to our example, we could do so without having to modify the synchronization rules of the Ptc-system net. In addition, they naturally define an interface for each module. It should be noted that while synchronized channels are used directly in the implementation in Renew, they are hidden behind a layer of abstraction in the formal definition. This is done because the synchronized channels are used for the specific purpose of allowing communication between modules via the synchronization rules. Consequently, channels in modules are all of the same type, namely uplinks, and channels with differing names can be matched according to synchronization rules. 4.1.4. Variables as arc weights Like the synchronized channels, the use of variables allows us to further aggregate actions of a similar function. If newly introduced producers/consumers differ by the amount they produce/consume, it suffices to introduce new possible bindings for the variables; no changes to the synchronization rules are needed. While the modular P/T-nets in [10] do not allow for such a functionality, the modular CP-nets in [15] do due to the use of colored Petri nets. 4.2. Formal Definition of Ptc-System Nets We now give the definition of a Ptc-system net. But first, we define a P/T net module, which acts as the basic building block of the Ptc-system net. Their difference from ordinary P/T-nets is that some transitions are external and can’t fire independently. Instead, they are assigned channels to allow synchronization. Additionally, arcs involving external transitions are allowed to hold variables as weights. Definition 10. A P/T-net module is a tuple 𝒩 = (𝑃, 𝑇, 𝐹, 𝑉 𝑎𝑟, 𝑊, 𝑚0 , 𝐾, 𝑇𝑒 , 𝐸, 𝑓 ), where: • 𝑃 is a finite set of places • 𝑇 is a finite set of transitions • 𝐹 ⊆ (𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ) the flow relation • 𝑉 𝑎𝑟 is a finite set of variables • 𝑊 : 𝐹 → N+ ∪ 𝑉 𝑎𝑟 the arc weight function • 𝑚0 : 𝑃 → N0 the initial marking • 𝐾 is a finite set of channels • 𝑇𝑒 ⊆ 𝑇 the set of external transitions 110 Simon Bott et al. CEUR Workshop Proceedings 104–121 • 𝐸 : 𝑇𝑒 → 𝐾 the channel assignment function • 𝑓 : 𝑇𝑒 → 2𝑉 𝑎𝑟×N0 the variable assignment function Further, we require that transitions with variables on incoming or outgoing arcs are external transitions, or more formally: ∀𝑡 ∈ 𝑇 : (∃𝑣 ∈ {𝑊 (𝑝, 𝑡) | 𝑝 ∈ 𝑃 } ∪ {𝑊 (𝑡, 𝑝) | 𝑝 ∈ 𝑃 } : 𝑣 ∈ 𝑉 𝑎𝑟) ⇒ 𝑡 ∈ 𝑇𝑒 (11) Now we have to adjust the enabling rules of a P/T-net module. Note that the extension 𝑊 ̃︁ of the arc weight function remains unchanged. 𝑡 Definition 11. A transition 𝑡 is enabled for a marking 𝑚, denoted by 𝑚 →, iff 𝑡∈ / 𝑇𝑒 ∧ ∀𝑝 ∈ 𝑃 : 𝑊 ̃︁ (𝑝, 𝑡) ≤ 𝑚(𝑝) (12) Now we get to the Ptc-system net, the overarching model that includes all modules, the synchro- nization rules that govern interactions between modules and potential variable assignments for each rule. Definition 12. A Ptc-system net is a tuple 𝒮𝒩 = (𝑆, 𝐾, 𝑅, 𝑉 𝑎𝑟, 𝑓𝑅 ), where: • 𝑆 is a finite set of P/T-net modules, whose places and transitions are pairwise disjoint • 𝐾 is a finite set of channels • 𝑅 ⊆ 𝐵𝑎𝑔(𝐾) the synchronization rules • 𝑉 𝑎𝑟 is a finite set of variables • 𝑓𝑅 : 𝑅 → 2𝑉 𝑎𝑟×N0 the variable assignment function Now follow some helpful definitions. First, some designators for the union of certain elements over all modules. Definition 13. For a given Ptc-system net 𝒮𝒩 = (𝑆, 𝐾, 𝑅, 𝑉 𝑎𝑟, 𝑓𝑅 ) with the P/T-net modules 𝑠 = (𝑃𝑠 , 𝑇𝑠 , 𝐹𝑠 , 𝑊𝑠 , 𝑚0𝑠 , 𝐾𝑠 , 𝑇𝑒𝑠 , 𝐸𝑠 , 𝑓𝑠 ) ∈ 𝑆 the following helpful definitions are introduced: ⋃︁ 𝑃 = 𝑃𝑠 (13) 𝑠∈𝑆 ⋃︁ 𝑉 𝑎𝑟 = 𝑉 𝑎𝑟𝑠 (14) 𝑠∈𝑆 ⋃︁ 𝑇 = 𝑇𝑠 (15) 𝑠∈𝑆 ⋃︁ 𝑇𝑒 = 𝑇𝑒𝑠 (16) 𝑠∈𝑆 𝑓 : 𝑇𝑒 ∪ 𝑅 → 𝑉 𝑎𝑟 × N0 (17) {︂ 𝑓𝑠 (𝑥) , if 𝑥 ∈ 𝑇𝑒𝑠 𝑓 (𝑥) = (18) 𝑓𝑅 (𝑥) , if 𝑥 ∈ 𝑅 Then we define the set of variables that is relevant when considering transitions that fire syn- chronously. Definition 14. The set of variables 𝑉 𝑎𝑟𝑇𝑚 that are weights of incoming or outgoing arcs of a transition in a multiset of transitions 𝑇𝑚 is defined as: 𝑉 𝑎𝑟𝑇𝑚 = {𝑥 | 𝑥 ∈ 𝑉 𝑎𝑟 ∧ ∃𝑝 ∈ 𝑃 ∃𝑡 ∈ 𝑇𝑚 : (𝑥 = 𝑊 (𝑝, 𝑡) ∨ 𝑥 = 𝑊 (𝑡, 𝑝))} (19) 111 Simon Bott et al. CEUR Workshop Proceedings 104–121 When transitions synchronize, they are best described by a multiset of participating transitions, which we call a synchronized firing group. Further, it has to fulfill conditions in that it must fit a synchronization rule and a valid assignment for all relevant variables must exist. This is a key idea of the Ptc-system net, because when we construct an ordinary P/T-net from a Ptc-system net, every synchronized firing group is going to be its own transition. Definition 15. The set 𝐺 ⊆ 𝐵𝑎𝑔(𝑇𝑒 ) contains the synchronized firing groups 𝑔 ∈ 𝐺, satisfying: (︃ )︃ ⨄︁ ∃𝑟 ∈ 𝑅 : {𝐸(𝑡)}𝑏 = 𝑟 (20) 𝑡∈𝑔 ⋃︁ ∧ ∀𝑥 ∈ 𝑉 𝑎𝑟𝑔 : ∃!𝑛 ∈ N0 : (𝑥, 𝑛) ∈ 𝑓 (𝑟) ∪ 𝑓 (𝑡) (21) 𝑡∈𝑔 Equation 20 ensures that the participating transitions match a synchronization rule. Equation 21 describes how the assignments of relevant variables result from the individual assignments defined for each participating transition and the matching synchronization rule. Further, Equation 21 ensures that the assignment of each relevant variable exists and is unique. In our example, Figure 1, the multiset {tp1, ts0}𝑏 is a valid synchronized firing group because the sum of their channels, {produce, store}𝑏 matches the synchronization rule, represented by t2, and the relevant variable 𝑥 is uniquely assigned the value 3. Definition 16. The second condition of a synchronized firing group (Equation 21) is the definition of a function. Extension with the identity function for the natural numbers results in the function 𝛽𝑔,𝑟 : 𝑉 𝑎𝑟𝑔 ∪ N0 → N0 : {︃ 𝑥 , if 𝑥 ∈ N0 𝛽𝑔,𝑟 (𝑥) = 𝑛 , if 𝑥 ∈ 𝑉 𝑎𝑟𝑔 ∧ (𝑥, 𝑛) ∈ 𝑓 (𝑟) ∪ ⋃︀ 𝑓 (𝑡) (22) 𝑡∈𝑔 This function 𝛽𝑔,𝑟 gives an unambiguous binding for all relevant variables 𝑉 𝑎𝑟𝑔 of any given synchronized firing group 𝑔. With it, we can now express the effect a firing group has on the marking of individual places. Definition 17. The arc weight function can be extended for the overarching Ptc-system net to include ̃︁𝑠𝑦𝑛𝑐 : (𝑃 × 𝐺) ∪ (𝐺 × 𝑃 ) → N0 : the synchronized firing groups with the extension 𝑊 ∑︁ 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑝, 𝑔) = 𝛽𝑔,𝑟 (𝑊 ̃︁ (𝑝, 𝑡)) (23) 𝑡∈𝑔 ∑︁ 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑔, 𝑝) = 𝛽𝑔,𝑟 (𝑊 ̃︁ (𝑡, 𝑝)) (24) 𝑡∈𝑔 Now we conclude by defining the enabling and firing rules of a Ptc-system net. Note that the enabling and firing rules of internal transitions, 𝑡 ∈ 𝑇 ∖ 𝑇𝑒 , follow from the definition of P/T-net modules (Definition 10). 𝑔 Definition 18. A synchronized firing group 𝑔 is enabled for a marking 𝑚, denoted by 𝑚 →, iff ∀𝑝 ∈ 𝑃 : 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑝, 𝑔) ≤ 𝑚(𝑝) (25) 𝑔 Definition 19. The successor marking 𝑚′ (𝑝) after firing a synchronized firing group 𝑔, denoted by 𝑚 → 𝑚′ , is defined as ∀𝑝 ∈ 𝑃 : 𝑚′ (𝑝) = 𝑚(𝑝) − 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑝, 𝑔) + 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑔, 𝑝) (26) We now shortly reexamine our example in Figure 1. The transitions t2 and t3 represent the two synchronization rules 𝑟t2 and 𝑟t3 . These induce the synchronized firing groups 𝑔t2 = {tp1, ts0} and 𝑔t3 = {tc1, ts1} with the assignments 𝛽𝑔t2 ,𝑟t2 (𝑥) = 3 and 𝛽𝑔t3 ,𝑟t3 (𝑥) = 2. 𝑔t3 is not enabled because 𝑊 ̃︁𝑠𝑦𝑛𝑐 (Storage, 𝑔t3 ) = 𝛽𝑔t3 ,𝑟t3 (𝑥) = 2 > 𝑚(Storage) = 0. 𝑔t2 , however, is 𝑔t2 enabled, and the markings before and after firing 𝑚 → 𝑚′ are given in the following table: 112 Simon Bott et al. CEUR Workshop Proceedings 104–121 𝑝 pReady pUnready cReady cUnready Capacity Storage 𝑚(𝑝) 1 0 1 0 5 0 𝑚′ (𝑝) 0 1 1 0 2 3 4.3. Construction of an Equivalent P/T-Net Our goal for this construction is the alternative definition of a P/T-net Definition 5. To that end, we construct pre and post for a given Ptc-system net. Definition 20. The matrices pre, post ∈ Z|𝑃 |×(|𝑇 ∖𝑇𝑒 |+|𝐺|) for a given Ptc-system net are as follows: pre𝑝𝑡 = 𝑊 ̃︁ (𝑝, 𝑡), with 𝑡 ∈ 𝑇 ∖ 𝑇𝑒 (27) pre𝑝𝑔 = 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑝, 𝑔) (28) post𝑝𝑡 = 𝑊 ̃︁ (𝑡, 𝑝), with 𝑡 ∈ 𝑇 ∖ 𝑇𝑒 (29) post𝑝𝑔 = 𝑊 ̃︁𝑠𝑦𝑛𝑐 (𝑔, 𝑝) (30) The components of a P/T-net have to be finite. 𝑃 and 𝑇 ∖ 𝑇𝑒 are unions of finite sets and therefore finite themselves. That leaves only 𝐺. Lemma 1. The set of firing groups 𝐺 for a given Ptc-system net is finite, so |𝐺| < ∞. Proof. Let 𝐺′ ⊆ 𝐵𝑎𝑔(𝑇𝑒 ) be the set of firing groups 𝑔 ′ ∈ 𝐺′ , that would result if we were to ignore the fit of variables (equation 20). Their only condition is: (︃ )︃ ⨄︁ ∃𝑟 ∈ 𝑅 : {𝐸(𝑡)}𝑏 = 𝑟 (31) 𝑡∈𝑔 If we also ignore the distinction between channels and consider the most complex synchronization rule 𝑟𝑚𝑎𝑥 ∈ 𝑅 as the upper bound for all synchronization rules, that satisfies: ∀𝑟 ∈ 𝑅 : |𝑟| ≤ |𝑟𝑚𝑎𝑥 | (32) Then follows the upper limit: |𝐺| ≤ |𝐺′ | ≤ |𝑅| · |𝑇𝑒 ||𝑟𝑚𝑎𝑥 | < ∞ (33) Now we can define the equivalent P/T-net. Definition 21. For a given Ptc-system net its equivalent P/T-net is given by the net 𝒩 = (𝑃, (𝑇 ∖ 𝑇𝑒 ) ∪ 𝐺, pre, post, 𝑚0 ), with 𝑚0 : 𝑃 → N0 being the initial marking of all modules combined. 5. Computing Invariants Calculation of invariants is a costly operation. In [15, 16] and [8] some relevant explanations are given how modular nets could support the calculations. Here we describe the calculation for our slightly different definition. 113 Simon Bott et al. CEUR Workshop Proceedings 104–121 5.1. Incidence Matrix From Definition 20 we also get the incidence matrix Δ = post − pre ∈ Z|𝑃 |×(|𝑇 ∖𝑇𝑒 |+|𝐺|) . We now choose a suitable ordering for the elements of Δ by grouping places and internal transitions for each module and placing the synchronized firing groups at the end. This treatment was used already in [4]. We get the incidence matrix in the following form: ⎛ ⎞ Δ 𝑠1 0 ··· ··· 0 Δ𝑐1 ⎜ 0 ⎜ Δ 𝑠2 0 ··· 0 Δ𝑐2 ⎟⎟ Δ = ⎜ ... .. .. .. ⎟ ⎜ . . . ⎟ (34) ⎜ ⎟ ⎝ 0 ··· 0 Δ𝑠𝑛−1 0 Δ𝑐𝑛−1 ⎠ 0 ··· ··· 0 Δ 𝑠𝑛 Δ 𝑐𝑛 The resulting matrix is now split into two parts. The first part is a block diagonal matrix with its submatrices Δ𝑠𝑖 describing the internal actions of each module, while the second part is a block matrix with a single column containing submatrices Δ𝑐𝑖 that describe the local effect of synchronized firing groups for each module. Note that the resulting incidence matrix is in the desired form for the approach described in [4], in which a parallel algorithm for computing invariants is given. 5.2. Differing Approaches to P- and T-Invariants The rows of submatrices of Δ can be viewed individually as the block matrices Δ𝑖 and used to compute invariants for each module. This leads to the following homogeneous systems of equations: (︀ )︀ Δ𝑖 = Δ𝑠𝑖 Δ𝑐𝑖 (35) (︂ )︂ 𝑥𝑠𝑖 Δ𝑖 𝑥𝑖 = 0, with 𝑥𝑖 = , 𝑥𝑠𝑖 ∈ Z|𝑇 ∖𝑇𝑒 | , 𝑥𝑐𝑖 ∈ Z|𝐺| (36) 𝑥𝑐𝑖 ΔT 𝑖 𝑦 𝑖 = 0, with 𝑦 𝑖 ∈ Z|𝑃𝑠𝑖 | (37) While the submatrix Δ𝑐𝑖 might at first glance seem very large, the number of different non-zero columns is closer to |𝑇𝑒𝑖 |, the number of external transitions in the module 𝑠𝑖 . Either synchronized firing groups don’t include transitions of 𝑠𝑖 , in which case the associated column is zero, or they include some linear combination of external transitions, in which case just the external transitions themselves need to be considered. Variables require a symbolic approach or add new non-zero columns for every different value they could be assigned. Therefore, the effort needed to compute the T-invariants for an individual module is comparable to the effort needed if it were an ordinary P/T-net. We know from [4] that T-invariants 𝑥𝑖 , 𝑥𝑗 of different modules 𝑠𝑖 , 𝑠𝑗 are the same part of a solution of the entire Ptc-system net if and only if they have the same coupling components 𝑥𝑐𝑖 , 𝑥𝑐𝑗 . This allows us to combine local T-invariants to derive T-invariants for the whole system. We know from Theorem 6.4 in [10] that if 𝑦 𝑖 is a P-invariant of an individual module 𝑠𝑖 then its extension for all places, where it is equal to zero for every place not in 𝑃𝑖 , is also a P-invariant of the entire Ptc-system net. 6. Verification Because P-invariants for individual modules are preserved in the context of the whole Ptc-system net, as shown in Section 5, properties that result from such P-invariants are preserved too. One such property is the structural boundedness resulting from positive P-invariants. If we consider the Producer in our example Figure 1, we find that it has the P-invariant ( 11 ). For the entire Ptc-system 114 Simon Bott et al. CEUR Workshop Proceedings 104–121 net, follows the P-invariant: ⎛ ⎞ 1 pReady ⎜1⎟ ⎜ ⎟ pUnready ⎜0⎟ ⎜ ⎟, cReady with the ordering (38) ⎜0⎟ ⎜ ⎟ cUnready ⎝0⎠ Capacity 0 Storage Since we have found a positive P-invariant spanning the places pReady and pUnready, we know that they are structurally bounded. The same can be done for Producer and Storage. Doing so results in the invariant that covers the whole net. ⎛ ⎞ 1 ⎜1⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ ⎜1⎟ (39) ⎜ ⎟ ⎝1⎠ 1 The internal logic of the modules in our example could also be expanded. We illustrate this in Figure 2, where we added a complex production process. The idea of no shared places as mentioned in 4.1.1 is also illustrated this way. Figure 2: Producer with internal production The place pUnready could be an implicit place that is refined by a whole subnet. The subnet contains the internal behavior of the net with the interface of transition t1 and its uplink :produce(3). All internal behavior is hidden through the transitions startproduction and endproduction. Further parts of the internal net are hidden. Assuming an invariant ensured in the internal net, this invariant can be calculated concurrently to all other internal nets in other net templates. It is important to notice that all P-invariants and T-invariants, provided they only include internal transitions, would be preserved in such internal processes. Furthermore, internal restriction on a net, e.g. being a correct workflow net (see [29]) could even speedup the calculations. What has not been discussed so far and is also not covered by the presented solutions here is the dynamic creation of net instances of net templates. This is an inherent feature of reference nets [26] and our Renew tool. With slightly modified definitions this also becomes possible. However, the 115 Simon Bott et al. CEUR Workshop Proceedings 104–121 mechanisms of introducing an arbitrary number of net instances provided by a net template as in reference nets would result in dynamic matrix dimensions. This is not covered by traditional invariant treatment and would make verification nearly impossible and hence we also do not cover this option here. In the following we will cover this feature partly when discussing the advantages for modeling. 7. Further Example We will now consider one more example to further illustrate the Ptc-system nets and verification method. (a) Client (b) Server Figure 3: A client sending request to the server and receiving success or fail responses. Figure 4: The system net creating the net instances. The example shown in Figure 3 models a simple client-server interaction. The client sends requests (the details are abstracted away) to the server and either gets a fail or success as a response. The client can concurrently prepare and send seven requests due to the seven tokens on p0. After sending the request, a token is placed in p3 to state that it is waiting for a response. If it receives a fail response, it corrects the request and sends it again; otherwise, it fills the Ready tokens on p0 again. The request 116 Simon Bott et al. CEUR Workshop Proceedings 104–121 exchange happens between the transitions that are named t0 in both nets via the synchronous channels. The synchronization can be seen in the SystemNet shown in Figure 4. On the server side, we have a request buffer (p0) to store up to five requests modeled with a complementary place (p1). The requests are processed one by one (increasing the tokens on p4 would allow concurrent processing) and produce randomly either a fail or success response, which are modeled by different places. The responses are sent via the respective synchronous channels. With the goal of finding invariants for the entire Ptc-system net, we first consider the invariants of the individual modules. The elements of the invariants are ordered by the names of the transitions/places in ascending order. For the Client net, we find two T-invariants 𝑥𝑐,0 , 𝑥𝑐,1 and one P-invariant 𝑦 𝑐,0 : ⎛ ⎞ ⎛ ⎞ 1 1 ⎛ ⎞ ⎜0⎟ ⎜1⎟ 1 ⎜ ⎟ ⎜ ⎟ ⎜1⎟ ⎜1⎟ , 𝑥𝑐,1 = ⎜0⎟ , 𝑥𝑐,0 = ⎜ 𝑦 𝑐,0 = ⎜ (40) ⎟ ⎜ ⎟ ⎟ ⎝1⎠ ⎝1⎠ ⎝0⎠ 1 0 1 For the Server net, we find two T-invariants 𝑥𝑠,0 , 𝑥𝑠,1 and two P-invariants 𝑦 𝑠,0 , 𝑦 𝑠,1 : ⎛ ⎞ ⎛ ⎞ ⎛ ⎞ ⎛ ⎞ 1 1 1 0 ⎜0⎟ ⎜1⎟ ⎜1⎟ ⎜0⎟ ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ⎜1⎟ ⎜0⎟ ⎜0⎟ ⎜1⎟ ⎜0⎟ , 𝑥𝑠,1 = ⎜1⎟ , 𝑥𝑠,0 = ⎜ ⎟ ⎜ ⎟ ⎜0⎟ , 𝑦 𝑠,1 = ⎜1⎟ 𝑦 𝑠,0 = ⎜ ⎟ ⎜ ⎟ (41) ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ⎝1⎠ ⎝0⎠ ⎝0⎠ ⎝1⎠ 1 1 0 1 We can now combine T-invariants with the same coupling components. They correspond to the transitions being synchronized, so t0𝑐 and t0𝑠 , t1𝑐 and t1𝑠 , t2𝑐 and t2𝑠 (we use subscripts to differentiate between modules). For example, 𝑥𝑐,0 and 𝑥𝑠,1 can’t be combined because their values differ between t1𝑐 and t1𝑠 . Their coupling components do not match. The coupling components of 𝑥𝑐,0 and 𝑥𝑠,0 , however, do match, and we can combine them to form the new T-invariant 𝑥0 . Similarly, we get 𝑥1 from 𝑥𝑐,1 and 𝑥𝑠,1 . The P-invariants stay preserved and can be expressed for the entire Ptc-system net by extending them with 0-entries. For the order of elements, we list the places of the Client module in ascending order, followed by the places of the Server module in ascending order. Thereby, we get 𝑦 0 from 𝑦 𝑐,0 , 𝑦 1 from 𝑦 𝑠,0 , and 𝑦 2 from 𝑦 𝑠,1 . 1 0 0 ⎛ ⎞ ⎛ ⎞ ⎛ ⎞ {t0𝑐 , t0𝑠 }𝑏 ⎛ ⎞ ⎛ ⎞ 1 1 ⎜1⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ {t1𝑐 , t1𝑠 }𝑏 ⎜1⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ {t2𝑐 , t2𝑠 }𝑏 ⎜1⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜1⎟ ⎜0⎟ t3𝑐 ⎜0⎟ ⎜1⎟ ⎜0⎟ 𝑥0 = ⎜ ⎜0⎟ , 𝑥1 = ⎜1⎟ , ⎟ ⎜ ⎟ with the ordering , 𝑦0 = ⎜ ⎜0⎟ , 𝑦 1 = ⎜1⎟ , 𝑦 2 = ⎜0⎟ ⎟ ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ t4𝑐 ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ t3𝑠 ⎜0⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ ⎝0⎠ ⎝1⎠ t4𝑠 ⎜0⎟ ⎜ ⎟ ⎜0⎟ ⎜ ⎟ ⎜1⎟ ⎜ ⎟ 1 0 t5𝑠 ⎝0⎠ ⎝0⎠ ⎝1⎠ 0 0 1 (42) 8. Discussion First of all it is important to notice that we do not work with traditional P/T-nets only. However, all presented versions can directly be mapped to P/T-nets. What is an important modeling advantage is that 117 Simon Bott et al. CEUR Workshop Proceedings 104–121 the formalism is relatively simple compared to Colored Petri Nets (see [30, 31]) or reference nets (see [26]). Synchronous channels provide additional power in terms of modeling capabilities, introducing new modeling options to P/T-nets. The approaches in [5, 9, 8] limited synchronization by allowing only two transitions to participate. This was done to avoid cyclic calls and possibly resulting infinite synchronizations. The Ptc-system net also avoids such synchronizations, but without any such restriction. As already identified in [10], the efficacy of the modular approach is inversely related to the extent of the synchronization between modules. In the worst case, every transition is external and has a unique channel. Then the Ptc-system net would just describe a majorly interconnected P/T-net and nothing would be gained, as there would be no modular structure to exploit. In the best case, there is no interaction between modules at all. The Ptc-system net would describe the union of its modules, and all modules could be viewed completely independently of one another. Well-structured nets will make limited use of the synchronization. One interpretation of the synchronization is to consider the synchronization of two nets via the synchronous channel as the communication of two objects or agents. This idea has been shown in [32, 33, 34] and heavily used in subsequent work in this field (see [35]). However, there the focus was on expressibility when modeling complex systems with elaborated communication concepts related to speech act theory [36]. For the Mulan nets [37, 11] so called Agent Interaction Protocol Diagrams are used to describe the communication (what is very similar to sequence diagrams from UML [38]). In [23] the relation to the HERAKLIT approach is introduced for a version concentrating on the underlying P/T-net structure of the relations between agents / HERAKLIT modules. Therefore our presented results can be applied to this area of work. Abstraction of modules is easy. Behind a net module more complex system parts can be hidden. By separating the channels of external and internal parts, behind the interfaces of a net module, arbitrary large further sets of net modules can communicate completely separated from the rest of the system (if the channels are disjunct from the channels of net modules outside the considered net module). Due to the high flexibility of the combination of synchronous channels, it is important to minimize the complexity of the synchronization. We believe this to be an advantage of the Ptc-system net in comparison to [10]. Allowing 𝑛 transitions with one channel 𝛼 to synchronize with 𝑚 transitions with another channel 𝛽 would require only a single synchronization rule. Meanwhile, it would require a transition fusion set for every possible combination, 𝑛 · 𝑚. If the 𝑚 transitions are all part of the same module and only differed by the values on some incoming and outgoing arcs, then our model could simplify them to a single transition that uses variables. Such a simplification is not possible in [10]. While we covered the preservation of P-invariants, there are also P-invariants that are newly intro- duced when introducing interaction between modules. These aren’t as easy to compute because more than individual modules have to be considered. However, the modular structure is still beneficial in their computation. Firstly, the incidence matrices of modules can be reduced into a more favorable form independently of one another, enabling parallel computation. Secondly, the synchronous channels make such reductions easier by reducing the number of differing columns. This also covers the ideas presented in [5]. A possible goal would be the reduction to an upper triangular form. Such a form could be used in state space construction [39]. While a subset of generating P-invariants could also be used, the full set would further minimize the space required to store markings of the state space. An alternative to conventional state space constructions would be the modular state space in [16, 10]. Because only modular P/T-nets without place fusions were considered, it is reasonable to expect that modular state spaces can also be applied to Ptc-system nets. However, further examination is required to determine how this would work in detail and whether synchronous channels would bring significant improvements. This directly follows the ideas presented in [5]. The independence of modules in regard to their properties resulting from P-invariants could allow making statements about modules added during runtime. This would lead to a natural extension of the Ptc-system net, where modules can be dynamically created and deleted with P/T-nets acting as patterns. To extend the net structure at execution / simulation time is an inherent feature of reference nets [26]. 118 Simon Bott et al. CEUR Workshop Proceedings 104–121 In Renew the idea of net templates that can be instantiated and deleted during the dynamic phase of a net, is an essential part of the tool [40]. The newly provided formalism for Renew covers the version of [5]. For our extension we are currently building an internal prototype to cover the formalism and to extend the work of [8]. Generally it is quite obvious that tool support with respect to modeling and verification are both very helpful. Another application, as also mentioned in [10, 5], is the independent calculation of the state space. However, in this contribution we do not deepen this discussion, as it falls in the same category as the abstraction of subsystems by separating the possibly shared channels. Currently, we work on the application of our Ptc-net formalism to model the control flow between software modules to cover orchestration and choreography of participating software modules. Each software module gets a net module assigned. The calls of methods that are part of the interface of the software module are covered by synchronized transitions. The software modules must then be rigorously restricted in order to follow the behavior of the net modules. The net modules must cover the complex software behavior without handling the actual values and functions to allow the mapping between software and net modules. First prototypes of this are build and successfully tested and will be covered by other work of the authors and their colleagues. 9. Conclusion An extension to former work of [10, 5] has been made to allow more complex synchronization of net modules that are coupled via synchronous channels. Due to the special perspective and used concepts the calculation of invariants are conceptually supported with respect to concurrent calculation of individual internal invariants and for the synchronization parts of the whole system. Our modular approach can allow for reduced complexity in the analysis of large systems. Removal of shared places allows conserving P-invariants of modules, and the introduction of syn- chronous channels can allow similar actions in the model to be condensed. Multisets are used at various points to express our definitions and are especially useful in allowing transitions to participate in firing groups more than just once. Further, T-invariants for the entire net result from combining the T-invariants of individual modules. Overall, verification can be done in a way that considers individual modules for most computations, thereby reducing runtimes and modeling of complex systems is directly supported by relating software modules / software components / services etc. to net modules. Options to combine Petri net modeling (supported by verification) with software engineering to ensure properties of e.g. plugin architectures is ongoing work. As tool support is a necessary condition we also improve our current software infrastructure Renew and the whole modeling approach Paose concurrently to the more theoretical work. References [1] S. Cayir, M. Uçer, An algorithm to compute a basis of Petri net invariants, in: 4th ELECO Int. Conf. on Electrical and Electronics Engineering. UCTEA, Bursa, Turkey, 2005. [2] J. Martínez, M. Silva, A simple and fast algorithm to obtain all invariants of a generalised Petri net, in: Application and Theory of Petri Nets: Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets Strasbourg, 23.–26. September 1980 Bad Honnef, 28.–30. September 1981, Springer, 1982, pp. 301–310. [3] C.-F. Law, B. Gwee, J. S. Chang, Optimized algorithm for computing invariants of ordinary Petri nets, in: 5th IEEE/ACIS International Conference on Computer and Information Science and 1st IEEE/ACIS International Workshop on Component-Based Software Engineering, Software Architecture and Reuse (ICIS-COMSAR’06), IEEE, 2006, pp. 23–28. [4] A. Bourjij, M. Boutayeb, T. Cecchin, A decentralized approach for computing invariants in large scale and interconnected Petri nets, in: 1997 IEEE International Conference on Systems, Man, and Cybernetics. Computational Cybernetics and Simulation, volume 2, IEEE, 1997, pp. 1741–1746. 119 Simon Bott et al. CEUR Workshop Proceedings 104–121 [5] L. Voß, S. Willrodt, D. Moldt, M. Haustermann, Between expressiveness and verifiability: P/T-nets with synchronous channels and modular structure, in: M. Köhler-Bußmeier, D. Moldt, H. Rölke (Eds.), Proceedings of the International Workshop on Petri Nets and Software Engineering 2022 co-located with the 43rd International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2022), Bergen, Norway, June 20th, 2022, volume 3170 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 40–59. URL: https://ceur-ws.org/Vol-3170. [6] E. Jessen, R. Valk, Rechensysteme: Grundlagen der Modellbildung, Studienreihe Informatik, Sprin- ger-Verlag, Berlin Heidelberg New York, 1987. [7] S. Christensen, N. D. Hansen, Coloured Petri Nets Extended with Channels for Synchronous Communication, Technical Report DAIMI PB-390, Aarhus University, 1992. [8] C. Künemund, Entwicklung eines Plugins zur Berechnung und Visualisierung von Invarianten in P/T-Netzen mit synchronen Kanälen in Renew, Bachelor thesis, University of Hamburg, Depart- ment of Informatics, Vogt-Kölln Str. 30, D-22527 Hamburg, 2021. [9] L. Voß, Development of a Formalism for P/T Nets with Synchronous Channels and their Analysis using Siphons and Traps in Renew, Bachelor thesis, University of Hamburg, Department of Informatics, Vogt-Kölln Str. 30, D-22527 Hamburg, 2022. [10] S. Christensen, L. Petrucci, Modular analysis of Petri nets, The Computer Journal 43 (2000) 224–242. [11] L. Cabac, Modeling Petri Net-Based Multi-Agent Applications, Dissertation, University of Hamburg, Department of Informatics, Vogt-Kölln Str. 30, D-22527 Hamburg, 2010. URL: https://ediss.sub. uni-hamburg.de/handle/ediss/3691. [12] K. Jensen, Coloured Petri nets and the invariant-method, Theoretical computer science 14 (1981) 317–336. [13] K. Jensen, How to find invariants for coloured Petri nets, in: International Symposium on Mathematical Foundations of Computer Science, Springer, 1981, pp. 327–338. [14] C. Lakos, L. Petrucci, Modular state spaces and place fusion, in: International Workshop on Petri Nets and Software Engineering (PNSE 2007, associated with Petri Nets 2007), 2007, pp. 175–190. [15] S. Christensen, L. Petrucci, Towards a modular analysis of coloured Petri nets, in: K. Jensen (Ed.), Application and Theory of Petri Nets 1992, 13th International Conference, Sheffield, UK, June 22-26, 1992, Proceedings, volume 616 of Lecture Notes in Computer Science, Springer, 1992, pp. 113–133. URL: https://doi.org/10.1007/3-540-55676-1_7. [16] S. Christensen, L. Petrucci, Modular state space analysis of coloured Petri nets, in: International Conference on Application and Theory of Petri Nets, Springer, 1995, pp. 201–217. [17] P. Fettke, W. Reisig, Handbook of Heraklit, 2021. Heraklit-working paper, v1.1, September 10, 2021, http://www.heraklit.org. [18] W. Reisig, Simple composition of nets, in: G. Franceschinis, K. Wolf (Eds.), Applications and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26, 2009. Proceedings, volume 5606 of Lecture Notes in Computer Science, Springer, 2009, pp. 23–42. URL: https://doi.org/10.1007/978-3-642-02424-5_4. doi:10.1007/978-3-642-02424-5\_4. [19] C. A. R. Hoare, Communicating sequential processes, Communications of the ACM 21 (1978) 666–677. [20] I. Sakellariou, I. Vlahavas, I. Futo, Z. Pasztor, J. Szeredi, Communicating sequential processes for distributed constraint satisfaction, Information Sciences 176 (2006) 490–521. [21] O. M. G. Inc., OMG Unified Modeling Language – version 2.5.1, https://www.omg.org/spec/UML/2.5.1, 2017. URL: https://www.omg.org/spec/UML/2.5.1, last accessed: 2024-06-05. [22] L. Cabac, D. Moldt, Formal semantics for AUML agent interaction protocol diagrams, in: J. Odell, P. Giorgini, J. P. Müller (Eds.), The Fifth International Workshop on Agent-Oriented Software Systems (AOSE-2004). Proceedings, Columbia University, New York, USA, 2004, pp. 97–111. URL: http://dx.doi.org/10.1007/978-3-540-30578-1_4. [23] D. Moldt, M. Hansson, L. Seifert, K. Ihlenfeldt, L. Clasen, K. Ehlers, M. Feldmann, Enriching heraklit modules by agent interaction diagrams, in: L. Gomes, R. Lorenz (Eds.), Application 120 Simon Bott et al. CEUR Workshop Proceedings 104–121 and Theory of Petri Nets and Concurrency - 44th International Conference, PETRI NETS 2023, Lisbon, Portugal, June 25-30, 2023, Proceedings, volume 13929 of Lecture Notes in Computer Science, Springer Nature Switzerland AG, Cham, Switzerland, 2023, pp. 440–463. URL: https: //doi.org/10.1007/978-3-031-33620-1_23. doi:10.1007/978-3-031-33620-1_23. [24] F. A. Heitmann, Algorithms and hardness results for object nets, Ph.D. thesis, Staats-und Univer- sitätsbibliothek Hamburg Carl von Ossietzky, 2013. [25] A. Syropoulos, Mathematics of multisets, in: Multiset Processing: Mathematical, Computer Science, and Molecular Computing Points of View 1, Springer, 2001, pp. 347–358. [26] O. Kummer, Referenznetze, Logos Verlag, Berlin, 2002. URL: http://www.logos-verlag.de/cgi-bin/ engbuchmid?isbn=0035&lng=eng&id=. [27] O. Kummer, F. Wienberg, M. Duvigneau, L. Cabac, M. Haustermann, D. Mosteller, Renew – the Reference Net Workshop, 2023. URL: http://www.renew.de/, release 4.1. [28] A. T. Cohen, Data abstraction, data encapsulation and object-oriented programming, ACM SIGPLAN Notices 19 (1984) 31–35. [29] W. v. d. Aalst, Verification of workflow nets, in: P. Azéma, G. Balbo (Eds.), Application and Theory of Petri Nets 1997, number 1248 in Lecture Notes in Computer Science, Springer Verlag, Berlin Heidelberg New York, 1997, pp. 407–426. [30] K. Jensen, Coloured Petri Nets: Volume 1; Basic Concepts, Analysis Methods and Practical Use, EATCS Monographs on Theoretical Computer Science, Berlin Heidelberg New York, 1992. [31] K. Jensen, L. M. Kristensen, Coloured Petri Nets - Modelling and Validation of Concurrent Systems, Springer, 2009. URL: https://doi.org/10.1007/b95112. doi:10.1007/b95112. [32] C. Maier, D. Moldt, Object coloured Petri nets – A formal technique for object oriented modelling, in: B. Farwer, D. Moldt, M.-O. Stehr (Eds.), Report FBI-HH-B-205/97: Proceedings of the Workshop on Petri Nets in System Engineering (PNSE’97), Hamburg, September 25-26, 1997, number FBI- HH-B-205/97 in Report of the Department of Informatics, University of Hamburg, Department of Computer Science, 1997, pp. 11–19. [33] C. Maier, D. Moldt, Dynamic structure and behaviour of coloured Petri nets supporting object- oriented modelling, in: W. van der Aalst, J.-M. Colom, F. Kordon, G. Kotsis, D. Moldt (Eds.), Petri Net Approaches for Modelling and Validation, LINCOM Studies in Computer Science, LINCOM Europa, München, 2002, pp. 81–101. [34] M. Köhler, D. Moldt, H. Rölke, Modelling the structure and behaviour of Petri net agents, in: J. Colom, M. Koutny (Eds.), Proceedings of the 22nd Conference on Application and Theory of Petri Nets 2001, volume 2075 of Lecture Notes in Computer Science, Springer-Verlag, 2001, pp. 224–241. URL: http://www.springerlink.com/link.asp?id=j4kbf32af81bba75. [35] L. Cabac, M. Haustermann, D. Mosteller, Software development with Petri nets and agents: Approach, frameworks and tool set, Sci. Comput. Program. 157 (2018) 56–70. URL: https://doi.org/ 10.1016/j.scico.2017.12.003. [36] J. R. Searle, Speech Acts, Cambride University Press, 1969. [37] H. Rölke, Modellierung von Agenten und Multiagentensystemen – Grundlagen und Anwendungen, volume 2 of Agent Technology – Theory and Applications, Logos Verlag, Berlin, 2004. URL: http: //logos-verlag.de/cgi-bin/engbuchmid?isbn=0768&lng=eng&id=. [38] J. Odell, H. van D. Parunak, B. Bauer, Extending UML for agents, in: G. Wagner, Y. Lesperance, E. Yu (Eds.), Agent-Oriented Information Systems. Workshop at the 17th National Conference on Artificial Intelligence (AAAI), AOIS 2000, 2000, pp. 3–17. [39] K. Schmidt, Using Petri net invariants in state space construction, in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2003, pp. 473–488. [40] D. Moldt, J. Johnsen, R. Streckenbach, L. Clasen, M. Haustermann, A. Heinze, M. Hansson, M. Feld- mann, K. Ihlenfeldt, RENEW: modularized architecture and new features, in: L. Gomes, R. Lorenz (Eds.), Application and Theory of Petri Nets and Concurrency - 44th International Conference, PETRI NETS 2023, Lisbon, Portugal, June 25-30, 2023, Proceedings, volume 13929 of Lecture Notes in Computer Science, Springer Nature Switzerland AG, Cham, Switzerland, 2023, pp. 217–228. URL: https://doi.org/10.1007/978-3-031-33620-1_12. doi:10.1007/978-3-031-33620-1_12. 121