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 efectiveness 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.
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 ofers 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 [
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 if (, ) ∈/ 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 [
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 diferent 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. 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
• 0 = ⋃︀∈{1,...,ℓ} 0 We call the modular Petri net for ℳ.
⎧⎪ (, ) for (, ) ∈ and ∈ | • (, ) = ⎨
(* , ) for (* , ) ∈ and * ∈ ( ), • = ⋃︀∈{1,...,ℓ} , • = ⋃︀∈{1,...,ℓ} | ∪ { | ∈ ℱ }, where is the fusion transition for ∈ ℱ , • = ⋃︀∈{1,...,ℓ}( ∩ ( × | ∪ | × )) ∪ {(, ) | ∈ ℱ , (, []) ∈ } ∪ {( , ) | ∈ ℱ , ( [], ) ∈ } ⎪ ⎩ ⎪ ⎩ ⎧⎪ (, ) for (, ) ∈ and ∈ | • (, ) = ⎨ (, * ) for (, * ) ∈ and * ∈ ( ), ∈ ℱ , = , ∈ {1, . . . , ℓ} ∈ ℱ , = , ∈ {1, . . . , ℓ}
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 • = ⋃︀∈ {(∙ ∪ ∙ ) × } • ((, ), ) ∈ , if (, ) ∈ ; (, (, )) ∈ , if (, ) ∈ • ((, ), ) = (, ); (, (, )) = (, ) for a ∈ • 0 = 0 ∩ ( × N) We append the index to each transition to distinguish their occurrences in diferent 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 (, ) ∈ |, if ∃ ∈ ℱ : (, ) ∈ and | = ∖ |. This results in a set of instances ℐ = {[1, 01], . . . , [ℓ, 0ℓ]}. (t1,1) (t1,2)
p3 p2 t2
p4
(b) The resulting Petri net system after combining
the modules 1 and 2, where the edge
between 1 and (1, 2) was lost.
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 [
It is desirable to allow a single module to be replicated, or instantiated multiple times with possibly diferent 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 diferent markings can
still lead to a reduction in the local reachability graph compared to the combined size of individual
modules[
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.
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 [
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[
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 developed 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 diferent concepts provide various degrees of freedom.
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}.
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 suficiently 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 suficient 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.
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 suficiently 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.
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 suficient 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.
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. Algorithm 1 Algorithm to find replications procedure FindReplications(, {1, ..., }, maxsize) global stop_nodes = ∅ 1 ← ⟨{ 1}⟩, ..., ← ⟨{ }⟩ 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
remove last shell from 1, ..., end if return ⟨1, ..., ⟩, ⟨ 1, ..., − 1⟩ end procedure ◁ Set of nodes not to be explored further ◁ Each replication consists of a sequence of steps ◁ Even radius = Outer shell contains only places Algorithm 2 Subroutine to find calculate the next expansion step 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
next_step ← next_step ∪ ∙ ∪ ∙ ∖ visited_nodes ∖ stop_nodes end for if next_step = ∅ then
fail end if end for return ⟨next_step1, ..., next_step⟩ end procedure ◁ If a module can’t expand, fail
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 bufer (see Fig. 2b). The bufer introduces synchronization points, which can reduce the efectiveness of the state space reduction achieved by the modular approach. ◁ Collect valid neighbors of nodes in previous Algorithm 3 Subroutine to find and resolve conflicts between expansion steps ◁ Even number of previous steps =^ current step contains places ◁ Future work: find partner in conflicting modules ◁ contains all nodes from previous steps
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 difer, 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 difer 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 difers 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. Algorithm 4 Subroutine to equalize the size of expansion steps
else 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 = ⋃︀∈step1∪...∪step signature for all : (N × N ↦→ N) ∈ do ← { ∈ step | signature = }, ∀ ∈ {1, ..., } if |1| = ... = || then next_step ← next_step ∪ , ∀ ∈ {1, ..., } next_step ← next_step ∪ {choose Min{|1|, ..., ||} nodes from } ◁ Future Work
end if end for return ⟨next_step1, ..., next_step⟩ end procedure
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 suficient 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 procedure CalculateIsomorphism(⟨1, ..., ⟩, ⟨step1, ..., step⟩) ← InducedSubgraph(, step ∪ ⋃︀∈ ) for all ∈ {2, ..., } do − 1 ← Isomorphism(1, ) if − 1 = ∅ then
fail end if end for return ⟨ 1, ..., − 1⟩ end procedure
The result of the aforementioned algorithm contains the identified replications 1, ..., , each represented 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 representation 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 diferent 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 ′() = ′ if () = ′ ∧ ∈ ⋃︀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 efectiveness 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 difering 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. (a) Modularization of the 2x2 SquareGrid (2 seeds)
(b) Modularization of ten dining philosophers (3
seeds)
The prototype implementation is written in Python for its development flexibility and library support.
It utilizes the widely known networkx library [
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 suficiently large replicated modules on several models.
Figure 2a shows the result of the algorithm on the SquareGrid model [
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 diferent 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, 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-toimplement 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.
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 nfid 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 efort. 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.
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 [
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 [
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 Figure 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 = [N1,m01] p2 {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 generate 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 unafected 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 eficiency increase achieved by modularization. The exploitation of t-invariants provides a legitimate way to approach the modularization of a Petri net system. The computational efort seems comparatively lightweight, so with the proposed extensions we see this method as an extensible enrichment in modularization.
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 diferently. 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 afected. However, the
eficiency 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 afects several instances. For more details on the
analysis of the modular state space and the structures required for it, we reference [
In [
The method for this is to partition the matrix using hypergraph partitioning.
Definition 14 (Hypergraph [
Thus, a graph is a special instance of a hypergraph, where every hyperedge connect exactly two vertices.
Definition 15 (Hypergraph Partitioning [
A hypergraph partitioning divides a hypergraph into a set of disjoint subsets 1 , 2 , . . . , ℓ . The
external hyperedges connect vertices from distinct partitions. In [
In [
Definition 17 (Balanced Partition, Balance Criterion [
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 difer. The hypergraph partitioning problem is defined as follows: Hypergraph ℓ, Partitioning Input: Hypergraph , ℓ ∈ Z+ Question: Find a balanced ℓ-partitioning Π = {1 , 2 , . . . , ℓ }, such that (Π) is minimal.
This problem is NP-hard [
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 suficient 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 difer 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 suficient 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 partitioning 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)}. (a) Petri net system .
(b) Incidence hypergraph of .
For solving the hypergraph partitioning problem, there exist several tools, like [
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 [
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
[
Definition 21 (-Connectivity, 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 [
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, if (∙ ∪ ∙ ) ∩ (∙ ′ ∪ ′∙ ) ̸= ∅. 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.
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 diferent 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 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 diferent 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 dificult to compare with the other methods, since it was aimed at a diferent 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 eficiently. 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 eficiently 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 ofers diferent 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 eficient.
The quality of a modularization is not only a measure of how closely the modules match a modularization 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.