Automatic Modularization of Place/Transition Nets Julian Gaede1 , Judith-Henrike Overath1 and Sophie Wallner1 1 UniversitΓ€t Rostock, 18051 Rostock, Germany ( @uni-rostock.de) Abstract Modular Petri nets provide a way to alleviate the state-space explosion problem. However, Petri nets are usually not described as a modular structure. In order to benefit from the advantages of modular state space analysis, the Petri net has to be decomposed into modules in advance. In this paper, we discuss various approaches to automatic modularization. One approach focuses on finding replicated modules in a Petri net, since the state space for those replications needs to be computed only once during analysis. An implementation based on the graph isomorphism problem shows the validity of this idea. The effectiveness of state space reduction by modularization is significantly influenced by the size of the individual modules and the size of the interfaces between them. If possible, the modules should exhibit internal behavior, i.e. have a certain minimum size and produce nontrivial strongly connected components in their reachability graphs. The interfaces should be as small as possible to avoid an overhead of synchronization behavior at the interfaces. To this end, we firstly present an approach that produces modules with meaningful internal behavior based on T-invariants. Secondly, we explain two approaches that use hypergraph cuts to minimize the size of interfaces. Keywords Petri Nets, Modular State Space, Replication, Modularization, 1. Introduction A modular Petri net consists of subnets that act independently of each other and are synchronized via interfaces. Modularization is the concept of transforming a Petri net system into an equivalent modular Petri net with independent components but common interfaces. Sometimes Petri net system models describe systems that consist of such components anyway. However, this encapsulation is not represented by the conventional Petri net system formalism. Modularization offers the possibility to make this information exploitable for analysis. Another application is the decomposition of models that would not be expected to have a modular structure. Especially for Petri net systems with identical structures, modularization provides a suitable solution as it is more robust with respect to small deviations in contrast to symmetry. Regarding the well-known example of the dining philosophers, the symmetry is broken as soon as one of the philosophers grabs the forks in the opposite order. Anyway, such a version of the dining philosophers can be modularized according to our methods. The idea of decomposing a Petri net system for analysis is not new. One way of forming components is clustering [1]. However, the clusters do not have to be disjoint and therefore do not act independently of each other. There is also the approach of forming a compositional state space [2]. Here, the state spaces of the individual Petri net system components are calculated individually and then a global state space of the entire Petri net system is derived. Since the partial state spaces must be completely available for further calculations, the components must be bounded. Modularization does not require this restriction; components can be unbounded in themselves and only become restricted through their embedding into a modular Petri net. In this paper, Section 2 first introduces all the necessary concepts in the domain of modular Petri nets, as the notation differs from the notation of conventional Petri net systems. Then, we continue exploring the issue of automatic modularization of Petri net systems with a focus on increasing efficiency in the analysis. A major advantage in the analysis of a modular state space arises from the fact that the original Petri net system might contain replicated components, for which it is sufficient to compute the state space once [3]. Therefore, Section 3 concentrates on finding replications in the Petri net. As a Petri net system is basically a graph, the idea of finding replications can be reduced to finding isomorphic subgraphs in a graph. An implementation shows the validity of PNSE’24, International Workshop on Petri Nets and Software Engineering, 2024 Β© 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 53 Julian Gaede et al. CEUR Workshop Proceedings 53–73 this approach. Section 4 presents further ideas on how to modularize a Petri net system; especially when no more replications are expected. This is the case, for example, when all replications have already been found in a Petri net system, but a sufficiently large part of the net is still unmodularized. Likewise, the ideas can also be applied to modularize replications that have already been found, for example, if they are still quite large. Here, however, modularization should not simply be done blindly, but based on the structure of the Petri net system. One approach makes use of transition invariants, which are considered an important indicator of nontrivial behavior. Thus, a modularization based on t-invariants is expected to generate modules with meaningful behavior. What impedes the analysis in the modularized Petri net is the synchronization behavior of the modules among each other. Therefore, it is a legitimate reason to want to keep this synchronization behavior rare. This can be achieved by modularizing Petri net system in a way that the interfaces between modules are as small as possible. For this, (hyper)graph theoretical concepts are consulted. 2. Preliminaries Definition 1 (Petri net system). A Petri net system is a tuple 𝑁 = [𝑃, 𝑇, 𝐹, π‘Š, π‘š0 ], where β€’ 𝑃 is a finite set of places, β€’ 𝑇 is a finite set of transitions with 𝑃 ∩ 𝑇 = βˆ…, β€’ 𝐹 βŠ† (𝑃 Γ— 𝑇 ) βˆͺ (𝑇 Γ— 𝑃 ) is the set of arcs, β€’ π‘Š : (𝑃 Γ— 𝑇 ) βˆͺ (𝑇 Γ— 𝑃 ) β†’ N is the weight function with π‘Š (π‘₯, 𝑦) = 0 iff (π‘₯, 𝑦) ∈ / 𝐹 and β€’ π‘š0 is the initial marking, where a marking in general is a mapping π‘š : 𝑃 β†’ N. We call 𝑃 βˆͺ 𝑇 the nodes of a Petri net system. For a node π‘₯ ∈ 𝑃 βˆͺ 𝑇 , βˆ™π‘₯ = {𝑦 | (𝑦, π‘₯) ∈ 𝐹 } the preset of π‘₯ and π‘₯βˆ™ = {𝑦 | (π‘₯, 𝑦) ∈ 𝐹 } the postset of π‘₯. We call βˆ™π‘₯ βˆͺ π‘₯βˆ™ the environment for a node π‘₯ ∈ 𝑃 βˆͺ 𝑇 . The objective is to generate a modular structure for a given Petri net system, such that the modular Petri net generated out of the structure is isomorphic to the given system. Therefore, we introduce concepts for describing a modular structure. We follow the notation established in [3]. Definition 2 (Module). A module is a place/transition Petri net 𝑁𝑖 = [𝑃𝑖 , 𝑇𝑖 , 𝐹𝑖 , π‘Šπ‘– ] for 𝑖 ∈ N where the set 𝑇𝑖 is assumed to be partitioned into subsets 𝑇𝑖|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ of internal transitions and 𝑇𝑖|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ of interface transitions. A module describes some part of the full model’s structure. To exhibit any behavior, a module needs to be instantiated by adding an initial marking. Definition 3 (Instance). An instance is a Petri net system [𝑁𝑖 , π‘š0𝑖 ] of module 𝑁𝑖 for 𝑖 ∈ N, where π‘š0𝑖 : 𝑃𝑖 β†’ N is an initial marking of 𝑁𝑖 . While each instance has some self-contained (or internal behavior), they may synchronize with other instances via their interface transitions. This synchronization is accomplished by combining interface transitions of different instances to a fusion transition to force them to fire simultaneously if all individual preconditions are met. The fusion is guided by fusion vectors. Definition 4 (Fusion Vector, Support). Let ℐ = {[𝑁1 , π‘š01 ], . . . , [𝑁ℓ , π‘š0β„“ ]} be a set of instances. A fusion vector 𝑓 ∈ (𝑇1|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ βˆͺ {βŠ₯}) Γ— Β· Β· Β· Γ— (𝑇ℓ|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ βˆͺ {βŠ₯}) is a vector of interface transitions of the instances or βŠ₯. An instance [𝑁𝑗 , π‘š0𝑗 ] participates in 𝑓 with its interface transition 𝑑 ∈ 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ if 𝑓 [𝑗] = 𝑑. If 𝑓 [𝑗] = βŠ₯, the instance does not participate in the fusion. The support 𝑠𝑒𝑝𝑝(𝑓 ) = {𝑑 | 𝑓 [𝑗] = 𝑑} of a fusion vector is the (nonempty) set of contained interface transitions. An instance can participate at most once in a given fusion, but the same interface transition can appear in multiple fusion vectors. We are now ready to collect all information needed for the composition of modules. 54 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Definition 5 (Modular Structure). A modular structure is a tuple β„³ = [ℐ, β„±], where ℐ = {[𝑁1 , π‘š01 ], . . . , [𝑁ℓ , π‘š0β„“ ]} is a set of instances of pairwise disjoint modules and β„± βŠ† (𝑇1|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ βˆͺ {βŠ₯}) Γ— Β· Β· Β· Γ— (𝑇ℓ|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ βˆͺ {βŠ₯}) is a set of fusion vectors. From this modular structure we can derive a modular Petri net system, where places, internal transitions, and initial markings are taken from the individual instances. Every fusion vector defines another transition that inherits all the arcs of the contained interface transitions and establishes connections across instances. Consequently, interface transitions that do not appear in any fusion set do not appear in the composition. This can be trivially worked around by adding a fusion vector with only this transition and βŠ₯ everywhere else. Definition 6 (Modular Petri Net, Fusion Transition). Let β„³ = [ℐ, β„±] be a modular structure. From β„³, we can derive a Petri net system 𝑁 = [𝑃, 𝑇, 𝐹, π‘Š, π‘š0 ], where ⋃︀ β€’ 𝑃 = π‘—βˆˆ{1,...,β„“} 𝑃𝑗 , ⋃︀ β€’ 𝑇 = π‘—βˆˆ{1,...,β„“} 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ βˆͺ {𝑑𝑓 | 𝑓 ∈ β„±}, where 𝑑𝑓 is the fusion transition for 𝑓 ∈ β„±, ⋃︀ β€’ 𝐹 = π‘—βˆˆ{1,...,β„“} (𝐹𝑗 ∩ (𝑃𝑗 Γ— 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ βˆͺ 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ Γ— 𝑃𝑗 )) βˆͺ {(𝑝, 𝑑𝑓 ) | 𝑓 ∈ β„±, (𝑝, 𝑓 [𝑗]) ∈ 𝐹𝑗 } βˆͺ {(𝑑𝑓 , 𝑝) | 𝑓 ∈ β„±, (𝑓 [𝑗], 𝑝) ∈ 𝐹𝑗 } ⎧ βŽ¨π‘Šπ‘— (𝑑, 𝑝) for (𝑑, 𝑝) ∈ 𝐹𝑗 and 𝑑 ∈ 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ βŽͺ β€’ π‘Š (𝑑, 𝑝) = π‘Šπ‘— (𝑑* , 𝑝) for (𝑑* , 𝑝) ∈ 𝐹𝑗 and 𝑑* ∈ 𝑠𝑒𝑝𝑝(𝑓 ), βŽͺ 𝑓 ∈ β„±, 𝑑 = 𝑑𝑓 , 𝑗 ∈ {1, . . . , β„“} ⎩ ⎧ βŽ¨π‘Šπ‘— (𝑝, 𝑑) for (𝑝, 𝑑) ∈ 𝐹𝑗 and 𝑑 ∈ 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ βŽͺ β€’ π‘Š (𝑝, 𝑑) = π‘Šπ‘— (𝑝, 𝑑* ) for (𝑝, 𝑑* ) ∈ 𝐹𝑗 and 𝑑* ∈ 𝑠𝑒𝑝𝑝(𝑓 ), βŽͺ 𝑓 ∈ β„±, 𝑑 = 𝑑𝑓 , 𝑗 ∈ {1, . . . , β„“} ⎩ ⋃︀ β€’ π‘š0 = π‘—βˆˆ{1,...,β„“} π‘š0𝑗 We call 𝑁 the modular Petri net for β„³. Note that the initial marking of the modular Petri net is well-defined since the domains of all π‘š0𝑗 are pairwise disjoint. To generate a modular structure from a non-modular Petri net, we only need to find a mapping that unambiguously assigns an instance to each place, thus we get a place set for every instance. The other components of the modular structure, from which we can deduce a modular Petri net, can be derived from this set of places as shown in the following lemma. Lemma 1 (Deducing a modular structure from a partitioning of places). Let 𝑁 = [𝑃, 𝑇, π‘Š, 𝐹, π‘š0 ] be a Petri net. Further, let {𝑃1 , . . . , 𝑃ℓ } be a partitioning of 𝑃 . For 𝑃𝑗 with 𝑗 ∈ {1, . . . , β„“}, we generate instance [𝑁𝑗 , π‘š0𝑗 ] with ⋃︀ β€’ 𝑇𝑗 = π‘βˆˆπ‘ƒπ‘— {(βˆ™π‘ βˆͺ π‘βˆ™) Γ— 𝑗} β€’ ((𝑑, 𝑗), 𝑝) ∈ 𝐹𝑗 , iff (𝑑, 𝑝) ∈ 𝐹 ; (𝑝, (𝑑, 𝑗)) ∈ 𝐹𝑗 , iff (𝑝, 𝑑) ∈ 𝐹 β€’ π‘Šπ‘— ((𝑑, 𝑗), 𝑝) = π‘Š (𝑑, 𝑝); π‘Šπ‘— (𝑝, (𝑑, 𝑗)) = π‘Š (𝑝, 𝑑) for a 𝑝 ∈ 𝑃𝑗 β€’ π‘š0𝑗 = π‘š0 ∩ (𝑃𝑗 Γ— N) We append the index 𝑗 to each transition to distinguish their occurrences in different instances. The fusion vectors can be constructed by identifying transitions which occur in multiple instances. For 𝑑 ∈ 𝑇 , we identify the modules where 𝑑 occurs as 𝑖𝑛𝑑𝑖𝑐𝑒𝑠(𝑑) = {𝑗 | (𝑑, 𝑗) ∈ 𝑇𝑗 }. Then we generate a fusion vector 𝑓 for all 𝑑 where |𝑖𝑛𝑑𝑖𝑐𝑒𝑠(𝑑)| > 1, so that 𝑓 [𝑗] = (𝑑, 𝑗) if 𝑗 ∈ 𝑖𝑛𝑑𝑖𝑐𝑒𝑠(𝑑) and βŠ₯ otherwise. We can distinguish internal and interfaces transitions for the instances as well. Therefore, we declare (𝑑, 𝑗) ∈ 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ , iff βˆƒπ‘“ ∈ β„± : (𝑑, 𝑗) ∈ 𝑓 and 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘›π‘Žπ‘™ = 𝑇𝑗 βˆ– 𝑇𝑗|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ . This results in a set of instances ℐ = {[𝑁1 , π‘š01 ], . . . , [𝑁ℓ , π‘š0β„“ ]}. 55 Julian Gaede et al. CEUR Workshop Proceedings 53–73 [N1,m01] [N2,m02] p1 p1 (t1,1) (t1,2) p3 (t1,1) (t1,2) p3 p2 t2 p4 p2 (t2,1) (t2,2) p4 (b) The resulting Petri net system after combining (a) An invalid modular structure where (𝑑1 , 2) is the modules 𝑁1 and 𝑁2 , where the edge be- not included in 𝑁1 despite being connected to tween 𝑝1 and (𝑑1 , 2) was lost. 𝑝1 Figure 1: An invalid modularization resulting in the loss of structure after combining the modules. Example 1. Figure 1 illustrates why it is required to include all connected transitions for a given place into the same module. The place 𝑝1 is included in module 𝑁1 and connected to (𝑑1 , 2), which is in another module. Since the composition rules for a modular Petri net [3] only concern themselves with fusion transitions, in this case (𝑑2 , 1) and (𝑑2 , 2), which are fused into 𝑑2 in the resulting net. The connection between 𝑝1 and (𝑑1 , 2) is not reconstructed, changing the behavior of the modular Petri net compared to the composition of the modules. 3. Modularization based on Replications It is desirable to allow a single module to be replicated, or instantiated multiple times with possibly different initial markings, since this makes sense from a modelling perspective, but also unlocks additional memory-savings during model checking. To distinguish between those replications, we extend instances by a unique identifier, and call them replicated instances or short: r-instances. Definition 7 (R-Instance). An r-instance is a Petri net system [𝑁𝑖 , 𝑗, π‘š0𝑗 ] of module 𝑁𝑖 , where 𝑗 ∈ N is an instance identifier and π‘š0𝑗 : 𝑃𝑖 β†’ N is an initial marking of 𝑁𝑖 . The definitions for the modular structure, fusion vectors and modular Petri net can be easily amended to accommodate this extension. A fusion vector can contain transitions from multiple r-instances of the same module, since the module would be copied for each instance when constructing the modular Petri net. To identify replicated modules, we represent the net structure of the given Petri net system as a net graph. The marking of places is irrelevant for this, as replicated modules with different markings can still lead to a reduction in the local reachability graph compared to the combined size of individual modules[3]. Definition 8 (Net graph). For a given Petri net 𝑁 = [𝑃, 𝑇, 𝐹, π‘Š, π‘š0 ], the net graph 𝐺 = [𝑉, 𝐸, 𝑐] is a directed, labeled graph, where β€’ 𝑉 =𝑃 βˆͺ𝑇 β€’ 𝐸=𝐹 β€’ 𝑐(𝑣) = 𝑝 if 𝑣 ∈ 𝑃 β€’ 𝑐(𝑣) = 𝑑 if 𝑣 ∈ 𝑇 β€’ 𝑐((𝑣, 𝑣 β€² )) = π‘Š (𝑣, 𝑣 β€² ) In the way we define a modular structure, the state space of instances of the same module (regardless the initial marking) can be analyzed based on one common state structure. In general, identical structures lead to identical behavior, which we do not need to analyze repeatedly. Therefore, it makes sense to identify identical substructures in the net graph, which we then can declare as instances of one module. 56 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Given a net graph, the ideal scenario would be to maximize the number of identical structures, i.e. isomorphic induced subgraphs. Those subgraphs should be larger than a minimum size to avoid the trivial solution where each vertex is a subgraph. This problem is germane to the Induced Subgraph Isomorphism problem or the more general Maximum Common Induced Subgraph problem, where for two given graphs one must determine whether one graph is an induced subgraph of the other resp. the two graphs have a common induced subgraph with a minimum size. Those problems are known to be NP-complete, as described in [4]. The problem might as well be associated with the Largest Subgraph With A Property problem [4], where the task is to find the maximum subgraph with a given property. Considering the repeated occurrence of a subgraph as a property does not serve as a standard graph property why this problem can be neglected. From the field of data mining, the challenge to find identical substructures in graphs is known as the frequent subgraph mining [5]. Expressing our problem as a frequent induced subgraph mining problem turned out to be unsuitable. Frequent subgraph mining in general does not consider induced subgraphs, which is mandatory for us [6]. There are also approaches for induced subgraphs but on the base of multiple graphs [7]. Another related field concerns itself with the identification of overrepresented sub-structures in a network, so-called motifs. The algorithms from this field can be broadly categorized into motif-centered and network-centered approaches. A motif-centered procedure requires a motif as part of its input, which makes it unsuitable for our application. Conversely, a network-centered method starts by enumerating all subgraphs for a given size and counts their occurrence in the graph[8]. However, the performance of these approaches tends to scale poorly with the size of the motifs. Since the state space reduction achieved by the modularization of a Petri net system is heavily impacted by the amount of internal behavior of its modules [3], it is desirable to identify larger substructures. Therefore, a network-centered approach isn’t appropriate either to find replicated modules with sufficient internal behavior. Besides maximizing the number of identical structures we impose additional constraints to a solution. When considering subgraphs of Petri nets, not every induced subgraph is a valid replication. For every place we require all connected transitions to be included in the instance of the place. Otherwise, the edges of an omitted transition to a place cannot be reconstructed in the construction of the modular Petri net as described in Definition 6. With the graph theoretical background of the suspected NP-completeness of our problem we devel- oped an incremental heuristic approach to identify identical substructures in a net graph. The main idea is to unfold the substructures circularly from selected starting points while preserving isomorphism between them. Therefore, we present a necessary criterion and multiple heuristic concepts that lead to a more or less precise starting point selection. The different concepts provide various degrees of freedom. 3.1. Finding Seed Candidates First, we need to identify potential candidates that can serve as starting points, or seeds, for detecting isomorphic substructures. Given the net graph 𝐺 of a Petri net system 𝑁 , we only consider place vertices, i.e. vertices with 𝑐(𝑣) = 𝑝 as candidates. As described above, a place requires all adjacent transitions to be in its instance, while a transition does not impose such constraints. Considering the net graph of a given Petri net system we introduce the signature of a vertex, determining the number of neighbor vertices for a given edge type. Definition 9 (Signature). For a vertex 𝑣 ∈ 𝑉 we define the signature as a mapping 𝑠 : 𝑉 β†’ (N Γ— N β†’ N), such that 𝑠(𝑣)(𝑖, π‘œ) = |{𝑣 β€² | 𝑐(𝑣, 𝑣 β€² ) = π‘œ, 𝑐(𝑣 β€² , 𝑣) = 𝑖}|. The signature gives an initial impression of the direct neighborhood of a vertex 𝑣, i.e. how many vertices are connected to 𝑣 via a certain combination of incoming and outgoing edges. Example 2. In the Petri net system presented in Fig. 1b, the places 𝑝1 and 𝑝2 would share the signature 𝑠(𝑝𝑖 ) = {(1, 0) ↦→ 1, (0, 1) ↦→ 1}, while 𝑠(𝑝3 ) = {(1, 0) ↦→ 1} and 𝑠(𝑝4 ) = {(1, 0) ↦→ 2}. 57 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Only place vertices with identical signature can serve as starting points, since all neighboring transitions have to be included, which would immediately lead to non-isomorphic modules. To determine the actual seeds using the information provided by the signature, it makes sense to consider the number of candidates for each signature. It appears that candidates that share an infrequent signature are more promising seed vertices, since vertices with a rare connectivity structure are more likely to have same function in the model. However, the fewer candidates share a signature, the harder it becomes to ensure a spacing between seeds which allows the modules to grow to a sufficiently large size before colliding with another. While there exist methods to find a set of vertices in a graph with maximum distance between each other, it is in many cases sufficient to select vertices with a large enough distance between them. To define such a distance, one could look towards a specified maximum module size or attempt to exploit structural properties of the Petri net system. Once a minimum distance π‘‘π‘šπ‘–π‘› has been found, suitable seeds can be identified by starting a simultaneous depth-limited BFS from all candidates with a shared signature. If the BFS from a candidate finishes without encountering another candidate’s nodes within π‘‘π‘šπ‘–π‘› /2 steps, this candidate can serve as a seed. Otherwise, a seed can be selected from each set of conflicting candidates. In the case that there are too few suitable candidates remaining, the requirements have to be relaxed, either by reducing π‘‘π‘šπ‘–π‘› or by restarting the selection process with candidates with another shared signature. Besides those systematic approaches, a randomized selection can be performed instead. While the candidates still have to share their signature, it can be beneficial to omit checking the distance between candidates and instead relying on the expansion algorithm to deal with the colliding modules. Developing improved heuristics for seed selection is an area of further research, as well as quantifying their impact on the quality of the resulting modularization. 3.2. Expanding outwards Regardless the method we determine seeds, we receive a set of 𝑛 starting points suitable for determining isomorphic starting points in the Petri net system. To find sufficiently large replicated modules, we greedily expand the modules outwards from those starting points under a set of guidelines that will be presented in the following. During the process, each module is represented by a list 𝑅𝑖 , which contains sets of vertices. Those sets will be called shells and contain the nodes which were newly added during each step. The outline of this algorithm can be found in Algorithm 1, and will be subsequently defined by explaining the sub-procedures. 3.2.1. Finding expansion candidates In each expansion step, we first calculate the maximum possible expansion step of each module and then successively reduce this step until either all conditions for replicated modules are met or a necessary reduction fails. Since the modules grow from center outwards, it is sufficient to consider only neighbors of vertices from the outermost shell of each module, which weren’t already introduced in previous shells. Additionally, we maintain a set of vertices which are forbidden from being included or explored due to having caused conflicts in previous steps. Due to the bipartite nature of Petri nets, as well as the fact that we required each seed vertex 𝑣𝑖𝑆 to be ∈ 𝑃 , the shells created by this approach alternate between containing only place or transition vertices, but never a mix of both. 3.2.2. Resolving conflicts between steps The first reduction of the expansion step is accomplished by detecting conflicts between the steps. In every odd step, the candidate shells only contain transitions, which are allowed to overlap between modules. While the transitions remain in the expansion step, we mark them as forbidden to explore further to prevent complications downstream, such as the conflicting modules attempting to explore along the same paths in future steps. 58 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Algorithm 1 Algorithm to find replications procedure FindReplications(𝑁, {𝑣1𝑆 , ..., 𝑣𝑛𝑆 }, maxsize) global stop_nodes = βˆ… ◁ Set of nodes not to be explored further 𝑅1 ← ⟨{𝑣1𝑆 }⟩, ..., 𝑅𝑛 ← ⟨{𝑣𝑛𝑆 }⟩ ◁ Each replication consists of a sequence of steps repeat step1 , ..., step𝑛 ← CalculateNextSteps(𝑁, βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩) step1 , ..., step𝑛 ← ResolveConflicts(βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩, ⟨step1 , ..., step𝑛 ⟩) if not all step sizes are equal then step1 , ..., step𝑛 ← EqualizeSteps(⟨step1 , ..., step𝑛 ⟩) end if ⟨𝜎1 , . . . , πœŽπ‘›βˆ’1 ⟩ ← CalculateIsomorphism(βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩, ⟨step1 , ..., step𝑛 ⟩) if any of the previous operations fail then break end if for all 𝑖 ∈ {1, ..., 𝑛} do R𝑖 += steps𝑖 end for until modules exceed maxsize if |𝑅1 | mod 2 = 0 then ◁ Even radius = Outer shell contains only places remove last shell from 𝑅1 , ..., 𝑅𝑛 end if return βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩, ⟨𝜎1 , ..., πœŽπ‘›βˆ’1 ⟩ end procedure Algorithm 2 Subroutine to find calculate the next expansion step procedure CalculateNextSteps(𝑁, βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩) global stop_nodes next_step1 , ..., next_step𝑛 ← βˆ… for all 𝑖 ∈ {1, ..., 𝑛} do last_step ← last element of 𝑅𝑖 ⋃︀ visited_nodes ← 𝑉 βˆˆπ‘…π‘– 𝑉 for all 𝑣 ∈ last_step βˆ– stop_nodes do ◁ Collect valid neighbors of nodes in previous step next_step𝑖 ← next_step𝑖 βˆͺ 𝑣 βˆ™ βˆͺ βˆ™ 𝑣 βˆ– visited_nodes βˆ– stop_nodes end for if next_step𝑖 = βˆ… then fail ◁ If a module can’t expand, fail end if end for return ⟨next_step1 , ..., next_step𝑛 ⟩ end procedure In every even step, the shells contain only place vertices, which have to be disjoint between modules, as stated in Lemma 1. The simplest method to handle overlapping places is to mark them as forbidden and remove them from the expansion step, as seen in Alg. 3. This is a point of concern for improving the quality of the resulting modularization, since it is likely to introduce small ”strips” of places which run between the edges of modules and act as a buffer (see Fig. 2b). The buffer introduces synchronization points, which can reduce the effectiveness of the state space reduction achieved by the modular approach. 59 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Algorithm 3 Subroutine to find and resolve conflicts between expansion steps procedure ResolveConflicts(βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩, ⟨step1 , ..., step𝑛 ⟩) global⋃︀stop_nodes 𝑉𝑖 ← π‘…βˆˆπ‘…π‘– 𝑅, βˆ€π‘– ∈ {1, ..., 𝑛} ◁ 𝑉𝑖 contains all nodes from previous steps for all 𝑖 ∈ {1, ..., 𝑛} do for all 𝑣 ∈ step𝑖 do if 𝑣 ∈ (step1 βˆͺ ... βˆͺ step𝑛 ) βˆ– step𝑖 or 𝑣 ∈ (𝑉1 βˆͺ ... βˆͺ 𝑉𝑛 ) βˆ– 𝑉𝑖 then conflicts ← conflicts βˆͺ {𝑣} stop_nodes ← stop_nodes βˆͺ {𝑣} end if end for if |𝑅𝑖 | mod 2 = 0 then ◁ Even number of previous steps =^ current step contains places step𝑖 ← step𝑖 βˆ– conflicts ◁ Future work: find partner in conflicting modules end if end for return ⟨step1 , ..., step𝑛 ⟩ end procedure 3.2.3. Equalizing the step sizes The next reduction of the expansion step concerns itself with the size of the individual shells. Since the process attempts to maintain isomorphic substructures after each expansion, an equal number of vertices has to be added to each module in a given step. If the step sizes differ, all candidate shells have to be reduced to the size of the smallest one. This procedure is show in Alg. 4. When deconstructing a Petri net system into modules, the inclusion of a place 𝑝 ∈ 𝑃 in a module requires the inclusion of all transitions 𝑑 ∈ 𝑇 : (𝑝, 𝑑) ∈ 𝐹 βˆͺ 𝐹 βˆ’1 in the same module. Thus, if the current expansion steps consist of transitions, but differ in size, it is impossible to remove transitions from a candidate shell, and this reduction of the steps has to fail. However, the inverse is not required, which allows us to remove places from candidate shells of expansion steps with an even number. One method of constructing equally sized subsets of shells with a higher likelyhood of resulting in an isomorphic graph utilizes an idea similar to the signature 𝑠, which we previously calculated for selecting the seed vertices: Since we are only concerned with the immediate next expansion step, we calculate a modified signature π‘ β€²π‘˜ (𝑣)(𝑖, π‘œ) = |{𝑐(𝑣, 𝑣 β€² ) = π‘œ, 𝑐(𝑣 β€² , 𝑣) = 𝑖, 𝑣 β€² ∈ π‘‰π‘˜π‘‰ 𝑖𝑠𝑖𝑑𝑒𝑑 }|, where π‘‰π‘˜π‘‰ 𝑖𝑠𝑖𝑑𝑒𝑑 is the union of all previous expansion steps. This way, π‘ β€²π‘˜ (𝑣) : (N Γ— N β†’ N) describes the connection structure of a node 𝑣 ∈ π‘‰π‘˜π‘†β„Žπ‘’π‘™π‘™ to only its neighbors in the module π‘˜. To preserve the isomorphism between modules, nodes 𝑣1 , ..., 𝑣𝑛 are only kept in the shells of their respective module π‘˜ when they have the same number of incoming and outgoing edges to the previous shell of the module, so π‘ β€²π‘˜ (𝑣1 ) = ... = π‘ β€²π‘˜ (𝑣𝑛 ). If there is the same number of vertices 𝑣𝑖 with the same signature π‘ β€²π‘˜ (𝑣𝑖 ), all of these vertices remain in the shell. If this number of vertices differs between modules, the shell with the smallest number determines how many vertices of the other shells are kept. The selection heuristic of these vertices is subject to further research. After each reduction procedure, it is possible that a candidate expansion step is completely empty. Whether the step was empty from the beginning because all neighbors of the previous shell were marked as forbidden, were removed because they conflicted with other modules or emptied because their specialized signature 𝑠′ didn’t match any of the other candidates, the algorithm can’t grow the modules in this step and therefore not in any future steps. In this case, the algorithm fails and returns the last valid modules. 60 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Algorithm 4 Subroutine to equalize the size of expansion steps procedure EqualizeSteps(βŸ¨π‘…1 , ..., 𝑅𝑛 ⟩, ⟨step1 , ..., step𝑛 ⟩) next_step1 , ..., next_step𝑛 ← βˆ… if |𝑅1 | mod 2 = 1 then ◁ Odd number of previous steps =^ current step contains transitions fail ◁ Transitions can’t be excluded from expansion end if for all 𝑣 ∈ step1 βˆͺ (οΈ€... βˆͺ step𝑛 do signature𝑣 ← (𝑖, π‘œ) ↦→ |{𝑣 β€² | π‘Š (𝑣 β€² , 𝑣) = 𝑖 ∧ π‘Š (𝑣, 𝑣 β€² ) = π‘œ}| )οΈ€ end for ⋃︀ signatures = π‘£βˆˆstep βˆͺ...βˆͺstep signature𝑣 1 𝑛 for all 𝑠 : (N Γ— N ↦→ N) ∈ π‘ π‘–π‘”π‘›π‘Žπ‘‘π‘’π‘Ÿπ‘’π‘  do 𝑠𝑖 ← {𝑣 ∈ step𝑖 | signature𝑣 = 𝑠}, βˆ€π‘– ∈ {1, ..., 𝑛} if |𝑠1 | = ... = |𝑠𝑛 | then next_step𝑖 ← next_step𝑖 βˆͺ 𝑠𝑖 , βˆ€π‘– ∈ {1, ..., 𝑛} else next_step𝑖 ← next_step𝑖 βˆͺ {choose Min{|𝑠1 |, ..., |𝑠𝑛 |} nodes from 𝑠𝑖 } ◁ Future Work end if end for return ⟨next_step1 , ..., next_step𝑛 ⟩ end procedure 3.2.4. Calculating isomorphisms The last step after performing the aforementioned reductions is to verify that the calculated expansion step maintains the isomorphism between the modules. The module graphs are obtained by constructing the graphs induced from the net graph by all vertices contained in all steps of each module. Due to Isomorphism being a problem in NP, this part consumes most of the runtime and is subject to several heuristic approaches to reduce the complexity. Since the isomorphism between the modules is transitive, it is sufficient to find an isomorphism πœŽπ‘– between each replica 𝑅𝑖 and 𝑅1 , and not necessary to check isomorphism between every pair of modules, which is shown in Alg. 5. If an isomorphism check fails, the expansion step can’t be performed and the algorithm fails, again returning the last previously valid modules. Otherwise, the expansion steps are added to their respective modules in preparation for the next iteration of the loop. Algorithm 5 Subroutine to check the isomorphism between modules ..., 𝑅𝑛 ⟩, ⟨step1 , ..., step𝑛 ⟩) procedure CalculateIsomorphism(βŸ¨π‘…1 , ⋃︀ 𝐺𝑖 ← InducedSubgraph(𝑁, step𝑖 βˆͺ π‘…βˆˆπ‘…π‘– 𝑅) for all 𝑖 ∈ {2, ..., 𝑛} do πœŽπ‘–βˆ’1 ← Isomorphism(𝐺1 , 𝐺𝑖 ) if πœŽπ‘–βˆ’1 = βˆ… then fail end if end for return ⟨𝜎1 , ..., πœŽπ‘›βˆ’1 ⟩ end procedure 61 Julian Gaede et al. CEUR Workshop Proceedings 53–73 3.2.5. Post-processing and improvements The result of the aforementioned algorithm contains the identified replications 𝑅1 , ..., 𝑅𝑛 , each rep- resented by a sequence of expansion steps, as well as the isomorphic mappings 𝜎1 , ..., πœŽπ‘›βˆ’1 , so that 𝜎1 is the mapping⋃︀between 𝑅1 and 𝑅2 . We can collect all places from a replication repre- sentation 𝑅𝑖 as 𝑃𝑖 = π‘…βˆˆπ‘…π‘– (𝑅 ∩ 𝑃 ), where 𝑃 is the set of places of the input ⋃︀ Petri net system. The set of all places not included in the replicated modules is 𝑃𝑛+1 = 𝑃 βˆ– π‘–βˆˆ{1,...,𝑛} 𝑃𝑖 . Since {𝑃1 , ..., 𝑃𝑛 , 𝑃𝑛+1 } is a partition of 𝑃 , it induces a modular structure β„³β€² = [ℐ β€² , β„± β€² ], with the set of instances ℐ β€² = {[𝑁1β€² , π‘šβ€²01 ], ..., [𝑁𝑛+1 β€² , π‘šβ€²0(𝑛+1) ]} according to lemma 1. To combine these replicated modules into replicated instances of a single module, we define a modular structure β„³ = [ℐ, β„±] as follows: β€’ ℐ = {[π‘π‘Ÿπ‘’π‘π‘™ , 𝑗, π‘š0𝑗 ] | 𝑗 ∈ {1, ..., 𝑛}} βˆͺ {[π‘π‘Ÿπ‘’π‘ π‘‘ , 𝑛 + 1, π‘š0(𝑛+1) ]}, where π‘š0𝑗 (𝑝) = π‘š(πœŽπ‘—βˆ’1 (𝑝)) for 𝑗 ∈ {1, ..., 𝑛} and π‘š0(𝑛+1) (𝑝, 𝑛 + 1) = π‘š(𝑝). β€’ β„± is calculated analogously to Lemma 1 combined with ℐ. Due to the nature of the expansion, the replicated module π‘π‘Ÿπ‘’π‘π‘™ is connected, while the rest module π‘π‘Ÿπ‘’π‘ π‘‘ may not be. Therefore, π‘π‘Ÿπ‘’π‘ π‘‘ can w.l.o.g be split into connected modules, which can further improve the state space reduction. The aforementioned algorithm can be improved in different areas by making assumptions about the isomorphic mappings between the modules. While the seed vertices are selected in a way that incentivizes them to be mapped onto each other early in the process, it is entirely possible for that to change after a few successful expansion steps. However, after some number π‘Ÿ of steps, we can observe that the isomorphic mapping only frequently changes for some πœ€ outermost shells of the modules, while the mapping is stable in shells which are closer to the center. With this assumption, we can reduce the size of the input graphs for the isomorphism problem. The more successful expansion steps are performed, the larger the graphs, but the more stable the center. Let π‘†π‘˜π‘– be the set of nodes included in the 𝑖-th shell of the π‘˜-th module, and π‘Ÿ be the index of the currently planned expansion step, with all necessary reductions already performed. Furthermore, let πœŽπ‘˜ be the isomorphic mapping from module π‘˜ to π‘˜ + 1 after step π‘Ÿ βˆ’ 1. ⋃︀ Previously, the graphs πΊπ‘˜ were induced by the set of vertices 0β‰€π‘–β‰€π‘Ÿ π‘†π‘˜π‘– . Under the aforementioned assumption, the size of this set can be reduced by only including vertices from an ”inner” shell if they’re connected to a vertex in an ”outer” shell. When calculating the new ⋃︀ isomorphic mapping πœŽπ‘˜β€² , we β€² β€² β€² 𝑖 introduce the additional constraint that πœŽπ‘˜ (𝑣) = 𝑣 iff πœŽπ‘˜ (𝑣) = 𝑣 ∧ 𝑣 ∈ 1β‰€π‘–β‰€π‘Ÿβˆ’πœ€ π‘†π‘˜ , so inner vertices are always mapped to other inner vertices without having to include all other inner vertices. Another application of this assumption can be found during the step size reductions. When a place 𝑝 is included in the candidate expansion steps of multiple modules, the simplest resolution is to include this place in neither module. However, as described before, this reduces the result quality by introducing strips of places along the module borders. To counteract this behavior, it would be preferable to allocate the conflict place to a module instead of excluding it entirely. Since the number of vertices has to be equal across the planned expansion steps, it is necessary to find places that can be included into the other steps without violating the isomorphism. Under the assumption that the isomorphism tends to be stable after some steps, the isomorphic mapping from the previous step can be utilized to identify those places. Further research and experiments are required to validate the effectiveness of this approach by examining the success rate of such an allocation. The last area where the previous isomorphic mappings can be used is during the equalization of the step size. When the expansion steps contain a differing number of places with the same signature, identically sized subsets of those places have to be identified. The previous isomorphism could be utilized similarly as during the conflict resolution described before: By extending the modified signature π‘ β€²π‘˜ to include the isomorphism, we reduce the flexibility of changing the mapping of recently included vertices, but in turn gain a more sound heuristic that can reduce backtracking or unnecessary failures. 62 Julian Gaede et al. CEUR Workshop Proceedings 53–73 (b) Modularization of ten dining philosophers (3 (a) Modularization of the 2x2 SquareGrid (2 seeds) seeds) Figure 2: Results of the FindReplications procedure 3.2.6. Implementation The prototype implementation is written in Python for its development flexibility and library support. It utilizes the widely known networkx library [9] to manage the graph data structures and, more importantly, check and calculate the isomorphisms between modules using an implementation of the VF2 algorithm[10]. Our presented algorithm performs the isomorphism checks in a loop, and while the heuristic described in the previous section can take some strain off of the calculations by reducing the size of the input graphs, there’s more performance to be gained. It is likely that a specialized implementation of the isomorphism check could exploit the iterative nature of its execution to reduce redundant calculations, which currently have to be performed anew in every call. The current implementation supports the selection of seed vertices via their signature, as well as basic strategies for conflict resolution and step size equalization. Because of its impact on the runtime, the isomorphism calculation accepts several parameters to control the size of the stable area in the center, which reduces the graph size. Despite lacking the more sophisticated strategies that utilize isomorphic mappings from previous iterations to allocate conflicting places to modules and improve the result quality during step size equalization, the implementation finds sufficiently large replicated modules on several models. Figure 2a shows the result of the algorithm on the SquareGrid model [11] with the two seed vertices encircled in the top left and bottom right. After five successful expansion steps, the two modules meet on the center places of their adjacent grid cells, highlighted by the dashed circle. At this point, the algorithm can’t expand further due to the missing ability to allocate places between modules, causing it to terminate. An allocation strategy would be able to resolve this conflict by allowing the top left module to expand to the right, but not downwards, leaving those places for the bottom right module. The same kind of results can be observed on larger versions of the model, especially when the expansion is performed from more than two seed places. The results of the automatic modularization of another model is shown in Figure 2b. This is a version of the well-known dining philosophers model with ten philosophers. Vertices in this model only have one of two different signatures, where one signature is shared only by the ten forks while the other is common to the remaining 40 places. This makes the forks much more desirable starting points. As in Figure 2a, modules are in conflict on places between each other, and again those conflicts could be resolved by the aforementioned method. While it is impossible to make out from the figure alone, 63 Julian Gaede et al. CEUR Workshop Proceedings 53–73 the philosopher to the right of the top module actually grabs his forks in the opposite order from his colleagues, which prevents the application of state space reduction methods using symmetries, but leaves this approach unfazed since the philosophers fully contained in the replications still share the same behavior. All in all, the current state of the implementation performs well in terms of result quality, especially for models which contain highly replicated structures. For models where the desired modules are less obvious to the naked eye, the prototype often terminates early due to its lacking conflict resolution abilities. Since the main goal of the prototype was originally to provide a framework for easy-to- implement validation of modularization ideas, the runtime performance was not a large concern during early stages of development. However, the described assumptions about the stability of isomorphic mappings between the centers of modules resulted in significant performance gains, especially for models with high connectivity, and we expect another boost from utilizing an iteration-optimized version of the isomorphism checking algorithm. 4. Non-Replicated Modularization Modularization based on replications improves the analysis of Petri net systems by reducing redundant state space. In this chapter we will highlight other methods in order to deal with situations where we cannot expect to find replications. For example, if all replications have already been found in a given Petri net system, the rest of the network may still be large. In this case, we then could try to modularize the rest of the network with other methods. Another case would be the reduction of already found replications. The previously described approach always tries to find the largest possible replications. The size of the replications is not limited upwards, as long as the propagation does not collide with other replications. The replications can therefore become rather big. To leverage the advantage of modularization even further, it is possible to continue modularizing a replica again using other methods. The additional modularization can then be transferred from the replica to the other without any additional effort. Although Definition 5 encourages us to distinguish between the concepts of module and instance, we decline to do so in this section. Since we assume here that we will not find any replicas, i.e. instances, that belong to the same module, the association to the structure of modules is not required. From now on we will only use the term instances as components of a modular Petri net. The goal remains the modularization of a given Petri net system, as described in Definition 6. With respect to the application cases described above, we do not mind whether the given Petri net system itself is a just created instance, the remaining Petri net system or a completely new net; in any case we can build a modular Petri net out the given net. The following approaches aim to generate a partitioning of the place set of a Petri net, which can then be converted into a modular structure as described in lemma 1. 4.1. T-Invariants Decompositional analysis based on the structure of a Petri net system is obvious because of the strong connection between structure and behavior of Petri net systems. In [12] they advance the analysis by adding hierarchy through the nested unit Petri nets model. The Problem of dividing a Petri net system into functional subnets, a net with a denoted set of input and output places, is discussed in [13]. Invariants for the modularization of Petri net systems have been used before; [14] used place invariants to abstract a set of places to one place. This abstracted Petri net system tends to be simpler to analyze. Our approach here is to use transition invariants to generate instances with significant internal behavior. Transition invariants are a criterion for cyclic, thus non-trivial behavior. A cycle in the state space responses to a transition invariant of the according Petri net system [15]. Note, that the existence of a transition invariant is only a necessary criterion for the existence of cyclic behavior; we may find a transition invariant we can never execute as it is not marked in any reachable marking. The use of t-invariants has already been used for the decomposition of Petri net systems due to their importance in the state space. In [1], a Petri net system is clustered on the basis of t-invariants, so that 64 Julian Gaede et al. CEUR Workshop Proceedings 53–73 resulting clusters correspond to functional units in biological networks. Here, however, the focus was on the clustering of similar invariants. Definition 10 (Incidence Matrix). A Petri net system 𝑁 = [𝑃, 𝑇, 𝐹, π‘Š, π‘š0 ] can be represented as an incidence matrix 𝐢 |𝑃 |Γ—|𝑇 | where 𝑐𝑖𝑗 = π‘Š ((𝑑𝑗 , 𝑠𝑖 )) βˆ’ π‘Š ((𝑠𝑖 , 𝑑𝑗 )) for 𝑖 ∈ {1, . . . , |𝑆|} and 𝑗 ∈ {1, . . . , |𝑇 |}. Definition 11 (Transition Invariants, Support). Let 𝑁 be a Petri net system and 𝐢 its incidence matrix. A transition invariant (t-invariant) ⃗𝑖 ∈ Z|𝑇 | is a solution of the homogenous linear system of equations 𝐢 Β· ⃗𝑖 = βƒ—0. The support 𝑠𝑒𝑝𝑝(𝑖⃗) βŠ† 𝑇 of the transition invariant ⃗𝑖 is the set of transitions whose entry is not zero in ⃗𝑖. Informally, a t-invariant describes a multiset of transitions whose execution will not change the state of the system. After firing all transitions, the net will be situated in the very same marking as before. |𝑇 | We only consider non-trivial, non-negative t-invariants. The trivial t-invariant βƒ—0 provides no useful information for us. A negative entry in a t-invariant would represent a reverse firing of a transition which is not applicable. Despite this restriction, we still can get infinitely many t-invariants. Therefore, we focus on minimal invariants. Definition 12 (Minimal Transition Invariants). For a minimal transition invariant ⃗𝑖 ∈ Z|𝑇 | , it exists no other t-invariant ⃗𝑖′ ∈ Z|𝑇 | with 𝑠𝑒𝑝𝑝(𝑖⃗′ ) βŠ‚ 𝑠𝑒𝑝𝑝(𝑖⃗) for ⃗𝑖′ ΜΈ= ⃗𝑖. Also, the least common divisor of the entries of ⃗𝑖 is 1. From now on, if we mention t-invariants, we always refer to minimal non-trivial, non-negative t-invariants, as we only consider those kinds of t-invariants. T-invariants serve as the bases for prospective instances of the modular Petri net. Instances should be disjoint per definition, thus we are only interested in t-invariants that have a disjoint set of support transitions. The requirement to compute disjoint t-invariants can be easily implemented in an iterative computation by claiming the weights of already computed support transitions to be zero in future invariants. Thus, they do not occur in support of further t-invariants. Even for disjoint t-invariants, the preplaces resp. postplaces of the support transitions may overlap. In accordance with the definition of instances in a modular structure, the sets of places need to be disjoint as well. To resolve this problem, we introduce the concept of super-disjointness. Definition 13 (Super-Disjointness). Let 𝑁 be a Petri net system and 𝐢 its incidence matrix. Two t-invariants ⃗𝑖, ⃗𝑖′ ∈ Z|𝑇 | are super-disjoint, if 1. they are disjoint, i.e. 𝑠𝑒𝑝𝑝(𝑖⃗) ∩ 𝑠𝑒𝑝𝑝(𝑖⃗′ ) = βˆ… ⋃︀ 2. the environments of the support transitions are disjoint as well; i.e. βƒ—) (βˆ™π‘‘ βˆͺ π‘‘βˆ™) ∩ π‘‘βˆˆπ‘ π‘’π‘π‘(𝑖 β€² β€² ⋃︀ 𝑑′ βˆˆπ‘ π‘’π‘π‘(𝑖⃗′ ) (βˆ™π‘‘ βˆͺ 𝑑 βˆ™) = βˆ… For a Petri net system, super-disjoint t-invariants can be calculated with a tool for Petri net system analysis, for example LoLA [16]. Calculating positive t-invariants is closely related to the integer linear programming problem, which is known to be NP-complete, therefore calculating t-invariants is not a trivial problem. Due to the restriction of super-disjointness, the calculation of will be executed |𝑇 | times worst case. We now assume we have generated a set ⋃︀ of super-disjoint t-invariants {𝑖⃗1 , . . . ,⃗𝑖ℓ }. From every βƒ— invariant 𝑖𝑗 , we generate a set of places 𝑃𝑗 = π‘‘βˆˆπ‘ π‘’π‘π‘(𝑖⃗𝑗 ) βˆ™π‘‘ βˆͺ π‘‘βˆ™ for 𝑗 ∈ {1, . . . , β„“}. With reference to Lemma 1, we can generate a modular structure out of the set of created place sets {𝑃1 , . . . , 𝑃ℓ }. Example 3 (super-disjoint T-Invariant Modularization). Let 𝑁 be a Petri net system, as depicted in Fig- ure 3a We can calculate three super-disjoint t-invariants 𝑖⃗1 , 𝑖⃗2 , 𝑖⃗3 , for which we can identify the support: 𝑠𝑒𝑝𝑝(𝑖⃗1 ) = {𝑑1 , 𝑑2 , 𝑑3 }, 𝑠𝑒𝑝𝑝(𝑖⃗2 ) = {𝑑4 , 𝑑5 } and 𝑠𝑒𝑝𝑝(𝑖⃗3 ) = {𝑑7 , 𝑑8 , 𝑑9 }. As described we generate the place set of the future instances from the environment of the support transitions. This results in 𝑃1 = 65 Julian Gaede et al. CEUR Workshop Proceedings 53–73 [N1,m01] (t1,1) t1 p1 [N2,m02] p1 p2 (t2,1) (t4,2) p4 p2 t2 t4 p4 (t3,1) p3 p5 (t5,2) t3 p3 p5 t5 (t6,1) (t6,2) (t6,3) t6 p6 (t7,3) (t10,3) (t10,4) p9 p6 t7 t10 p9 p7 (t9,3) (t11,4) p7 t9 t11 [N4,m04] (t8,3) p8 t8 p8 [N3,m03] (a) The original Petri net System 𝑁 . (b) A modularized version of 𝑁 based on t-invariants. Figure 3: Exemplary representation of the modularization of Petri net system 𝑁 . {𝑝1 , 𝑝2 , 𝑝3 }, 𝑃2 = {𝑝4 , 𝑝5 } and 𝑃3 = {𝑝6 , 𝑝7 , 𝑝8 }. The only place 𝑝9 of the rest net determines another instance with 𝑃4 = {𝑝9 }. According to Lemma 1, we can generate the modular structure. Firstly, we gen- erate the transition sets corresponding to the four place sets: 𝑇1 = {(𝑑1 , 1), (𝑑2 , 1), (𝑑3 , 1), (𝑑6 , 1)}, 𝑇2 = {(𝑑4 , 2), (𝑑5 , 2), (𝑑6 , 2)}, 𝑇3 = {(𝑑6 , 3), (𝑑7 , 3), (𝑑8 , 3), (𝑑9 , 3), (𝑑10 , 3)} and 𝑇4 = {(𝑑10 , 4), (𝑑11 , 4)}. Arcs and Weights and initial markings are defined appropriately. We can deduce that 𝑑6 of 𝑁 is a fusion transition and (𝑑6 , 𝑖) ∈ 𝑇𝑖|π‘–π‘›π‘‘π‘’π‘Ÿπ‘“ π‘Žπ‘π‘’ for 𝑖 ∈ {1, 2, 3}. The same applies for 𝑑10 and (𝑑10 , 𝑖) for 𝑖 ∈ {3, 4}. All other transitions of the instances are internal ones. This leads to two fusion vectors β„± = {[(𝑑6 , 1), (𝑑6 , 2), (𝑑6 , 3)], [(𝑑10 , 3), (𝑑10 , 4)]}. The modular Petri net generated out of the modular structure is depicted in Figure 3b. It is reasonable to assume instances generated on t-invariants do not modularize the Petri net system completely. Parts of the original Petri net system may remain unaffected by the modularization and form one instance by itself. That these parts are connected is improbable, therefore the analysis of this rest-instance would require a lot of synchronization with other instances. This is not consistent with the concept of individual analysis of the instances, which will accelerate the modular state space analysis. Furthermore, we assume that t-invariants tend to generate small instances with little internal behavior. It is therefore convenient to combine partial instances under certain conditions to form a larger instance. The most obvious approach is to join two instances that share a fusion set. This can be accomplished by unifying the place sets of the two instances and forming a new instance according to Lemma 1. This is possible without restriction, since the place sets are disjoint by construction. It is also possible to combine instances that are close to each other. For this purpose, we can calculate the shortest path between two instances in pairwise order. The goal is to merge the instances and to include the nodes on this shortest path into the new instance. In order to realize this, we extract the places that are located on the shortest path and join them with the union of the place sets of the instances. The whole set then serves as the basis for a new, larger instance. In this way, residual parts of the Petri net system, that lie between two instances are to be included in one instance. Doing so creates connected instances, which tend to have more internal behavior. It also reduces the unmodularized part of the Petri net system. The instances should not become too large, of course. It is recommended to define a maximum size for instances as the analysis of (too) large instances can reduce the efficiency increase achieved by modularization. The exploitation of t-invariants provides a legitimate way to approach the modularization of a Petri net system. The computational effort seems comparatively lightweight, so with the proposed extensions we see this method as an extensible enrichment in modularization. 66 Julian Gaede et al. CEUR Workshop Proceedings 53–73 4.2. Minimal Interfaces Another legitimate goal for modularization is the generation of the smallest possible interfaces. For the analysis of the state space of a modular Petri net, internal transitions and interface transitions of instances are treated differently. For the activation and firing of internal transitions only the state of the corresponding instance is relevant. The firing behavior of interface transitions depends on the states of all attached instances. The analysis must therefore include all instances affected. However, the efficiency increase of the analysis of modular state spaces follows from restricting the analysis to single instances. It is therefore a valid modularization criterion to keep the number of interface transitions as low as possible and thus to reduce behavior that affects several instances. For more details on the analysis of the modular state space and the structures required for it, we reference [3]. This subsection provides two approaches to generate a modular Petri net system with little interface behavior. 4.2.1. Modularization by Hypergraph Partitioning In [17], a system described only as an incidence matrix between states and actions is also to be modularized to speed up the analysis. Here, the data flow between the resulting modules should be minimized, i.e. the interface actions should be kept as small as possible. Finding minimal data flow between modules refers to the problem of finding a minimal cut. The method for this is to partition the matrix using hypergraph partitioning. Definition 14 (Hypergraph [18]). A hypergraph 𝐻 = [𝑉 𝐻 , 𝐸 𝐻 ] is defined as a set of vertices 𝑉 𝐻 and a set of hyperedges 𝐸 𝐻 between the vertices. A hyperedge 𝑒 ∈ 𝐸 𝐻 is a subset of vertices: 𝑒 βŠ† 𝑉 𝐻 . Thus, a graph is a special instance of a hypergraph, where every hyperedge connect exactly two vertices. Definition 15 (Hypergraph Partitioning [18]). Let 𝐻 = [𝑉 𝐻 , 𝐸 𝐻 ] be a hypergraph. The set of vertex sets Ξ  = {𝑉1𝐻 , 𝑉2𝐻 , . . . , 𝑉ℓ𝐻 } is an l-partition of 𝐻, if the following conditions hold: β€’ each set 𝑉𝑖𝐻 is a nonempty subset of 𝑉 𝐻 , i.e. βˆ… = ΜΈ 𝑉𝑖𝐻 βŠ† 𝑉 for 𝑖 ∈ {1, . . . , β„“} β€’ the sets are pairwise disjoint, i.e. 𝑉𝑖𝐻 ∩ 𝑉𝑗𝐻 = βˆ… for 𝑖 ΜΈ= 𝑗 ∈ {1, . . . , β„“} β€’ the union of all sets results in 𝑉 𝐻 , i.e. π‘–βˆˆ{1,...,β„“} 𝑉𝑖𝐻 = 𝑉 𝐻 ⋃︀ 𝐻 We refer to 𝐸𝑒π‘₯π‘‘π‘’π‘Ÿπ‘› = {𝑒 ∈ 𝐸𝐻 | βˆƒπ‘£π‘– ΜΈ= 𝑣𝑗 ∈ π‘’βˆƒπ‘‰π‘–π» ΜΈ= 𝑉𝑗𝐻 ∈ 𝑉 𝐻 : 𝑣𝑖 ∈ 𝑉𝑖𝐻 ∧ 𝑣𝑗 ∈ 𝑉𝑗𝐻 } as the external hyperedges. A hypergraph partitioning divides a hypergraph into a set of disjoint subsets 𝑉1𝐻 , 𝑉2𝐻 , . . . , 𝑉ℓ𝐻 . The external hyperedges connect vertices from distinct partitions. In [17], they reduce the problem of generating as little data flow as possible to hypergraph β„“-partitioning with minimal cost for β„“ > 0. The cost of a partitioning is related to the number of external hyperedges in the following way: Definition 16 (Cost of a Hypergraph Partitioning). Given a hypergraph 𝐻 = [𝑉 𝐻 , 𝐸 𝐻 ], the cost of an β„“-partitioning Ξ  = {𝑉1𝐻 , 𝑉2𝐻 , . . . , 𝑉ℓ𝐻 } is defined as πœ†(Ξ ) = |𝐸𝑒π‘₯π‘‘π‘’π‘Ÿπ‘› 𝐻 |. In [18], they additionally present a balance criterion. Definition 17 (Balanced Partition, Balance Criterion [18]). Let 𝐻 = [𝑉 𝐻 , 𝐸 𝐻 ] be a hypergraph and Ξ  = {𝑉1𝐻 , 𝑉2𝐻 , . . . , 𝑉ℓ𝐻 } an β„“-partitioning of 𝐻. For every vertex 𝑣 ∈ 𝐻 βˆ‘οΈ€π‘‰ , 𝑀(𝑣) denotes a weight 𝐻 𝐻 of 𝑣. For every partition 𝑉𝑖 for 𝑖 ∈ {1, . . . , β„“}, we define 𝑀(𝑉𝑖 ) = π‘£βˆˆπ‘‰ 𝐻 𝑀(𝑣) as the weight of 𝑖 𝑉𝑖𝐻 . Over all partitions, we can calculate the average weight of the partitions: π‘€π‘Žπ‘£π‘” = π‘˜π‘–=1 𝑀(𝑉𝑖𝐻 )/π‘˜. βˆ‘οΈ€ Partition Ξ  is said to be balanced if it fulfills the balance criterion: 𝑀(𝑉𝑖𝐻 ) ≀ π‘€π‘Žπ‘£π‘” (1 + πœ€). Here, πœ€ denoted a predefined maximum imbalance ratio allowed. The bigger we set πœ€, the more the partitions are permitted to differ. The hypergraph partitioning problem is defined as follows: 67 Julian Gaede et al. CEUR Workshop Proceedings 53–73 Hypergraph β„“, Partitioning Input: Hypergraph 𝐻, β„“ ∈ Z+ Question: Find a balanced β„“-partitioning Ξ  = {𝑉1𝐻 , 𝑉2𝐻 , . . . , 𝑉ℓ𝐻 }, such that πœ†(Ξ ) is minimal. This problem is NP-hard [19]. Therefore, we do not expect to find a hypergraph partitioning with the minimal cost; however, a heuristic approximate solution satisfies our requirements. The following step is an interpretation of a Petri net system as a hypergraph, for which we then aim to generate a balanced partitioning with minimal cost. Therefore, we introduce the incidence hypergraph. Definition 18 (Incidence Hypergraph). Given a Petri net system 𝑁 = [𝑃, 𝑇, 𝐹, π‘Š, π‘š0 ], the incidence hypergraph 𝐼 = [𝑉 𝐼 , 𝐸 𝐼 ] is an undirected, bipartite graph, where β€’ 𝑉𝐼 =𝑃 β€’ 𝐸 𝐼 = π‘π‘Žπ‘”π‘ (βˆ™π‘‘ βˆͺ π‘‘βˆ™ | 𝑑 ∈ 𝑇 ) (with π‘π‘Žπ‘”π‘ (𝑋) being a multiset with elements from 𝑋. ) Note, that in contrast of the Definition 14, the set of edges is defined as a multiset of subsets of places. The reason is, that for a Petri net system, the hyperedges should represent the transitions. The conventional hypergraph definition would compress transitions with the same set of pre/postplaces to one hyperedge, so structural information about the Petri net system would be neglected. For example, consider Petri net system 𝑁 in Figure 4a. If we add a transition 𝑑0 with βˆ™π‘‘0 = {𝑝2 } and 𝑑0 βˆ™ = {𝑝1 }, this would result in a hyperedge {𝑝1 , 𝑝2 }, which is already part of 𝐸 𝐼 representing transition 𝑑1 . Consequentially, no additional edge would be introduced and 𝑑0 becomes invisible. To avoid this, we adapt the definition for the use case of Petri net systems. As the weights are not important, the incidence hypergraph abstracts this information. For incidence hypergraph 𝐼 we aim to generate a balanced β„“-partition Ξ  = {𝑉1𝐼 , 𝑉2𝐼 , . . . , 𝑉ℓ𝐼 } with minimal cost πœ†(Ξ ). In our use case, we can weaken the balancing criterion formulated in Definition 17. As for now, the places of a Petri net system that form the vertices of the incidence hypergraph are all equally valid, we can neglect the weight of the vertices. To us, it is sufficient to have partitions with approximately the same size. Definition 19 (Balance Criterion for Incidence Hypergraph Partitioning). Let 𝐼 = [𝑉 𝐼 , 𝐸 𝐼 ] be an incidence hypergraph of a Petri net system 𝑁 and Ξ  = {𝑉1𝐼 , 𝑉2𝐼 , . . . , 𝑉ℓ𝐼 } an β„“-partitioning of 𝐻. Partitioning Ξ  is balanced, if every partition 𝑉𝑖𝐼 for 𝑖 ∈ {1, . . . , β„“} fulfills the following balance criterion: |𝑉𝑖𝐼 | ≀ |𝑉 𝐼 |/β„“ Β· (1 + πœ€). Each partition must not differ in size by more than πœ€-fold from the average size of a partition. Solving the hypergraph partitioning problem for the incidence hypergraph of a Petri net system will result in a partitioning of places and an identification of transitions as internal and interface. This information is sufficient to build a modular Petri net. Partition Ξ  divides the vertices of the incidence hypergraph 𝐼 into partitions {𝑉1𝐼 , 𝑉2𝐼 , . . . , 𝑉ℓ𝐼 }. If we take this down to the Petri net system level, the partitions correspond place sets {𝑃1 , 𝑃2 , . . . , 𝑃ℓ }, such that 𝑃𝑗 = 𝑉𝑗𝐼 for 𝑗 ∈ {1, . . . , β„“}. Each place set 𝑃𝑗 then forms the place set of an instance [𝑁𝑗 , π‘š0𝑗 ] for 𝑗 ∈ {1, . . . , β„“}. In accordance to Lemma 1 and with reference to our initially given Petri net system 𝑁 , we can generate a modular structure, thus a modular Petri net out of {𝑃1 , 𝑃2 , . . . , 𝑃ℓ }. Due to the balance criterion, the instances are approximately the same size while keeping the number of fusion transitions as small as possible. Example 4. Let 𝑁 be a given Petri net system, depicted in Figure 4a. For 𝑁 , we generate the incidence hypergraph 𝐼, depicted in Figure 4b. A balanced 2-partitioning for 𝐼 would be Ξ  = 𝐼 {{𝑝1 , 𝑝2 , 𝑝3 }, {𝑝4 , 𝑝5 , 𝑝6 }} with only one external hyperedge 𝐸𝑒π‘₯π‘‘π‘’π‘Ÿπ‘› = {{𝑝3 , 𝑝4 , 𝑝5 }}. This parti- tioning is balanced, as the partitions are the same size, and minimal - less than one hyperedge would not be possible for a connected underlying Petri net system. A resulting modular structure would contain two instances [𝑁1 , π‘š01 ], [𝑁2 , π‘š02 ], where 𝑃1 = {𝑝1 , 𝑝2 , 𝑝3 }, 𝑇1 = {(𝑑1 , 1), (𝑑2 , 1), (𝑑3 , 1)} and 𝑃2 = {𝑝4 , 𝑝5 , 𝑝6 } and 𝑇2 = {(𝑑3 , 2), (𝑑4 , 2), (𝑑5 , 2)}. The other components are defined appropriately. The only fusion set would be 𝑓 = {(𝑑3 , 1), (𝑑3 , 2)}. 68 Julian Gaede et al. CEUR Workshop Proceedings 53–73 p1 p4 {p1,p2} p1 p2 p3 p6 {p1,p2,p3} t1 t2 t3 t4 t5 {p3,p4,p5} p3 p4 {p4,p5} p5 p6 p2 p5 {p4,p5,p6} (a) Petri net system 𝑁 . (b) Incidence hypergraph 𝐼 of 𝑁 . Figure 4: Incidence hypergraph of a given net For solving the hypergraph partitioning problem, there exist several tools, like [18] or [20]. In [21], they provide a parallel approach to handle the severity of the problem. The problem remains NP-hard, which is why the approaches are only heuristic. In our case, the application of hypergraph partitioning may not necessarily deliver optimal results, nevertheless, in the following subsection we want to consider an approach which solves another applicable problem in polynomial time. 4.2.2. Modularization by Dual Hypergraph Cutting In this chapter, we highlight a method for modularizing Petri net systems using the dual incidence hypergraph. For this purpose, further graph-theoretic definitions are required. Definition 20 (Dual Hypergraph [22]). Let 𝐻 = [𝑉 𝐻 , 𝐸 𝐻 ] be a hyphergraph. The dual hypergraph 𝐻 * = [𝑉 𝐻* , 𝐸 𝐻* ] is a hypergraph, where 𝑉 𝐻* = 𝐸 𝐻 and 𝐸 𝐻* = {{𝑒 | 𝑒 ∈ 𝐸 𝐻 ∧ 𝑣1 ∈ 𝑒}, {𝑒 | 𝑒 ∈ 𝐸 𝐻 ∧ 𝑣2 ∈ 𝑒}, . . . , {𝑒 | 𝑒 ∈ 𝐸 𝐻 ∧ 𝑣𝑛 ∈ 𝑒}} for {𝑣1 , 𝑣2 , . . . , 𝑣𝑛 } = 𝑉 𝐻 . The edges of the hypergraph form the vertices of the dual hypergraph. For every vertex of a hypergraph, the set of hyper edges that contain this vertex corresponds to one edge of the dual hypergraph. The hypergraph partitioning problem from Section 4.2.1 seeks interdisjoint sets of vertices connected by as few hyperedges as possible. The equivalent problem in the dual hypergraph now aims to find the smallest possible set of vertices to remove, such that the graph is no longer connected without this set [22]. Such a set of vertices is called a minimal cut in graph theory. To approach this concept, we first define the connectivity of a graph. Definition 21 (π‘˜-Connectivity, Vertex Connectivity [23]). Let π‘˜ ∈ N. A Graph 𝐺 = [𝑉, 𝐸] is k- connected, if |𝑉 | > π‘˜ and every subgraph 𝐺 βˆ’ 𝑋 for 𝑋 βŠ† 𝑉 with |𝑋| < π‘˜ is connected. The maximum π‘˜ for that 𝐺 is π‘˜-connected, we call the vertex connectivity πœ…(𝐺). In other words, the πœ…(𝐺) defines a number of vertices we need to remove to destroy the connectivity of a graph. We can describe the set of vertices we need to remove more precisely as the minimal cut in a graph. Definition 22 (Minimal Cut). For a Graph 𝐺 = [𝑉, 𝐸], a subset 𝑋 βŠ† 𝑉 is a minimal cut, if 𝐺 βˆ’ 𝑋 is not connected and |𝑋| = πœ…(𝐺). By removing a minimal cut, the connectivity of the graph is broken, and the graph decomposes into components that are not connected to each other. A minimal cut of a hypergraph can be found by computing a minimal cut of its 2-section. Any minimal cut in 𝐻 is also a minimum cut in [𝐻]2 and vice versa. Definition 23. 2-Section [22] Let 𝐻 = [𝑉 𝐻 , 𝐸 𝐻 ] be a hypergraph. The 2-section of 𝐻 is an undirected graph [𝐻]2 = (𝑉 𝐻 , 𝐸2 ) where 𝑒 ∈ 𝐸 𝐻 : {π‘₯, 𝑦} βŠ‚ 𝑒 β‡’ {π‘₯, 𝑦} ∈ 𝐸2 . 69 Julian Gaede et al. CEUR Workshop Proceedings 53–73 t1 {t1,t2} {t1,t2} t1 t2 t2 t3 {t2,t3} {t3,t4,t5} t4 t3 t4 t5 {t3,t4,t5} {t5} t5 (a) Dual Incidence hypergraph 𝐼 * of 𝐼. (b) 2-Section [𝐼 * ]2 of 𝐼 * . Figure 5: Dual Incidence hypergraph and 2-section Thus, the 2-section of a hypergraph 𝐻 contains all vertices of 𝐻 and connects two vertices, if there is at least one hyperedge that contains those two vertices. In other words, the 2-section represents which vertices of 𝐻 are connected to each other. As described in [24], a minimal cut can be found in polynomial time. To use this knowledge to generate instances for a modular Petri net, we first generate the dual * * incidence hypergraph 𝐼 * = [𝑉 𝐼 , 𝐸 𝐼 ] to incidence hypergraph 𝐼 for a given Petri net system 𝑁 , as defined in Definition 20. In 𝐼 * the vertices correspond to the transitions of 𝑁 ; an edge represents a set of adjacent transitions for a particular place. Second, we create the 2-section of 𝐼 * as in Definition 23: * * [𝐼 * ]2 = [𝑉 𝐼 , 𝐸2* ], where 𝑉 𝐼 = 𝑇 and {𝑑, 𝑑′ } ∈ 𝐸2 , iff (βˆ™π‘‘ βˆͺ π‘‘βˆ™) ∩ (βˆ™π‘‘β€² βˆͺ 𝑑′ βˆ™) ΜΈ= βˆ…. Thus, the 2-section [𝐼 * ]2 contains all transitions of 𝑁 as vertices. Two vertices are connected if the according transitions share a place in their environments. A minimal cut 𝑋 of [𝐼 * ]2 gives a set of transitions, we need to remove to disconnect the graph. This cut 𝑋 leads to a set of external edges in the incidence hypergraph 𝐼 𝐸𝑒π‘₯π‘‘π‘’π‘Ÿπ‘› ; edges that lead from one partition of the incidence hypergraph to another partition of vertices. Vertices correspond to places of the underlying Petri net system, thus, we get a partitioning {𝑃1 , . . . , 𝑃ℓ } of 𝑃 . With Lemma 1 we can deduce a modular structure which we can transform into a modular Petri net. Notice, that the generated partitioning is not necessarily balanced. Example 5. For incidence hypergraph 𝐼 in Figure 4b, we generate the dual incidence hypergraph 𝐼 * , where the vertices correspond to the transitions of 𝑁 (cf. Figure 4a) and an edge represents a set of transitions that share one place in their environment. For example the edge {𝑑1 , 𝑑2 } expresses the fact, that 𝑑1 and 𝑑2 share one place, i.e. 𝑝1 . They are connected with two distinct arcs, with is which is evident from the fact that they also share two places, 𝑝2 in addition to 𝑝1 . The same holds for the transitions 𝑑3 , 𝑑4 and 𝑑5 . The 2-section of 𝐼 * is presented in Figure 5b. Here, the number of shared places is abstracted. Only the fact that two transitions are connected can be inferred from this representation. The main issue with this approach is the lack of control over the number and size of instances. A minimal cut separates the net into at least two components, but possibly more. Furthermore, no formulation of a balancing criterion is possible, i.e. the size of the modules is not balanced; the focus here is only on finding a minimum cut. Cutting the dual incidence hypergraph leads to optimal, i.e. minimal sets of fusion transitions but possibly to the detriment of the size and number of modules. 5. Conclusion and Future Work This paper provides approaches to automatically modularize Petri net systems. The main advantage in the modular state space analysis arises from the fact that several instances of the same module share the same state space if they have an analogous initial marking. Instances of the same module with different initial markings are still likely to have overlapping state spaces. These properties can be exploited during analysis to drastically reduce memory requirements. Therefore, the obvious approach to modularization is to first attempt to find replications. To incentivize that the replications contain 70 Julian Gaede et al. CEUR Workshop Proceedings 53–73 neither too little nor too much internal behavior, the FindReplications algorithm is controlled by a parameter which gives an upper bound for module size. If the identified replications are too small, the procedure can be restarted with a different set of seeds in an attempt to find another modularization with bigger modules. A prototype implementation shows the validity of the proposed method for models containing highly replicated structures, while yielding a starting point for improvements on less suitable models. Further improvements of the conflict handling employed by the process, of which several where suggested in 3.2, can push the point of termination further into the future, allowing the algorithm to find larger replicated modules. After replications have been identified, further modularization methods can be applied. This can be used to further modularize both the remaining Petri net system and the replications themselves. If a replicated module is further modularized, the results can be propagated to its other instances via the isomorphic mappings, which are computed during the process. In addition to replication finding, three other methods were presented. The first method, based on t-invariants, is rather difficult to compare with the other methods, since it was aimed at a different target. Here, the focus was on generating instances with nontrivial behavior. For this purpose, the concept of super-disjointness was introduced in order to derive disjoint instances from transition invariants. Those can be calculated efficiently. We also hope that the second method presented, based on hypergraph partitioning, will have an impact on module size, and thus behavior as well. Although this does not directly require the modules to have a certain size and structure, the balancing criterion expects the modules to be generated in a similar size. However, the main goal of this method was to minimize the interface behavior. This is achieved by finding a minimal β„“-partitioning of the incidence hypergraph, as which the Petri nets system is represented for this purpose. The major drawback of this method is that the hypergraph partitioning problem is NP-hard and thus rather heuristically generated solutions can be expected. The third method overcomes this disadvantage and provides a way to efficiently generate minimal interfaces. The idea is to represent the Petri net system as a dual hypergraph and then determine a minimal cut. This leads directly to a partition of the places of the Petri net system and thus to a valid modularization. But here, too, we have to make concessions. With this approach, the instances generated can be of arbitrary size. The minimal cuts also may generate a variable number of instances. Based on the fact that the method of hypergraph partitioning allows a balancing criterion, which controls both - the module size and the interface size - we consider this method to be the most promising. Also supporting this is that hypergraph partitioning can be performed well in parallel. Future Work might be an implementation of the other methods to compare their performance. The goal is to develop an implementation that offers different approaches to modularization. Those can be applied depending on the structure of the given Petri net system, resulting in the best possible modularization. This also includes further considerations of the structure. For example, net classes such as state machine or marked graph could be identified as distinct instances, making the analysis more efficient. The quality of a modularization is not only a measure of how closely the modules match a modu- larization performed by a model designer. Instead, it is also measured by the amount of state space reduction gained during analysis of a modular Petri net compared to its unmodularized counterpart. To evaluate our presented methods further in that regard, tool support is required to generate the full modular state space. A quantitative way to measure result quality would open up a more in-depth way of finding generally suitable parameters, as well as exploring ways to calculate fitting parameters from the structure of the given Petri net model. References [1] E. Grafahrend-Belau, F. Schreiber, M. Heiner, A. Sackmann, B. H. Junker, S. Grunwald, A. Speer, K. Winder, I. Koch, Modularization of biochemical networks based on classification of Petri net t-invariants, BMC Bioinformatics 9 (2008). 71 Julian Gaede et al. CEUR Workshop Proceedings 53–73 [2] P. Buchholz, P. Kemper, Hierarchical Reachability Graph Generation for Petri Nets, Formal Methods in System Design 21 (2002) 281–315. [3] J. Gaede, S. Wallner, K. Wolf, Modular State Spaces - A New Perspective, 2024. Accepted at Petri Nets Conference 2024. [4] M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP- Completeness, A Series of Books in the Mathematical Sciences, W. H. Freeman, New York, 1979. [5] M. Kuramochi, G. Karypis, Finding Frequent Patterns in a Large Sparse Graph, Data Mining and Knowledge Discovery 11 (2005) 243–271. [6] V. T. T. Duong, K. U. Khan, B.-S. Jeong, Y.-K. Lee, Top-k Frequent Induced Subgraph Mining Using Sampling, in: Proceedings of the Sixth International Conference on Emerging Databases: Technologies, Applications, and Theory, EDB ’16, Association for Computing Machinery, New York, NY, USA, 2016, pp. 110–113. [7] A. Inokuchi, T. Washio, H. Motoda, An Apriori-Based Algorithm for Mining Frequent Substructures from Graph Data, in: D. A. Zighed, J. Komorowski, J. Ε»ytkow (Eds.), Principles of Data Mining and Knowledge Discovery, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2000, pp. 13–23. [8] E. Wong, B. Baur, S. Quader, C.-H. Huang, Biological Network Motif Detection: Principles and Practice, Briefings in Bioinformatics 13 (2012) 202–215. [9] A. A. Hagberg, D. A. Schult, P. J. Swart, Exploring network structure, dynamics, and function using networkx, in: G. Varoquaux, T. Vaught, J. Millman (Eds.), Proceedings of the 7th Python in Science Conference, 2008, pp. 11 – 15. [10] L. P. Cordella, P. Foggia, C. Sansone, M. Vento, A (sub) graph isomorphism algorithm for matching large graphs, IEEE transactions on pattern analysis and machine intelligence 26 (2004) 1367–1372. [11] T. Shmeleva, D. Zaytcev, I. Zaytcev, Analysis of square communication grids via infinite petri nets (2009). [12] H. Garavel, Nested-unit petri nets: A structural means to increase efficiency and scalability of verification on elementary nets, in: R. R. Devillers, A. Valmari (Eds.), Application and Theory of Petri Nets and Concurrency - 36th International Conference, PETRI NETS 2015, Brussels, Belgium, June 21-26, 2015, Proceedings, volume 9115 of Lecture Notes in Computer Science, Springer, 2015, pp. 179–199. [13] D. Zaitsev, Decomposition of petri nets, Cybernetics and Systems Analysis 40 (2004) 739–746. [14] C. Lakos, On the Abstraction of Coloured Petri Nets, in: Application and Theory of Petri Nets 1997, volume 1248, Springer Berlin Heidelberg, Berlin, Heidelberg, 1997, pp. 42–61. [15] K. Schmidt, Using Petri Net Invariants in State Space Construction, in: H. Garavel, J. Hatcliff (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2003. [16] K. Wolf, Petri Net Model Checking with LoLA 2, in: V. Khomenko, O. H. Roux (Eds.), Applica- tion and Theory of Petri Nets and Concurrency, Lecture Notes in Computer Science, Springer International Publishing, Cham, 2018, pp. 351–362. [17] A. Ben Khaled El Feki, Distributed Realtime Simulation of Numerical Models : Application to Power-Train (2014). [18] Ü. CatalyΓΌrek, C. Aykanat, PaToH (Partitioning Tool for Hypergraphs), in: D. Padua (Ed.), Encyclopedia of Parallel Computing, Springer US, Boston, MA, 2011, pp. 1479–1487. [19] T. Lengauer, Combinatorial Algorithms for Integrated Circuit Layout, Springer Science & Business Media, 2012. [20] G. Karypis, V. Kumar, Metis: A Software Package for Partitioning Unstructured Graphs, Partitioning Meshes, and Computing Fill-Reducing Orderings of Sparse Matrices (1997). [21] A. Trifunovic, W. J. Knottenbelt, Parkway 2.0: A Parallel Multilevel Hypergraph Partitioning Tool, in: International Symposium on Computer and Information Sciences, Springer, 2004, pp. 789–800. [22] M. Dewar, D. Pike, J. Proos, Connectivity in Hypergraphs, Canadian Mathematical Bulletin 61 (2018) 252–271. Publisher: Cambridge University Press. [23] R. Diestel, Graphentheorie, 5 ed., Springer Spektrum, Berlin, 2017. 72 Julian Gaede et al. CEUR Workshop Proceedings 53–73 [24] M. Stoer, F. Wagner, A Simple Min-Cut Algorithm, Journal of the ACM (JACM) 44 (1997) 585–591. 73