Concurrency is an important aspect of Petri nets to describe and simulate the behavior of complex systems. Knowing which places and transitions could be executed in parallel helps to understand nets and enables analysis techniques and the computation of other properties, such as causality, exclusivity, etc.. All techniques based on concurrency detection depend on the efficiency of this detection methodology. Kovalyov and Esparza have developed algorithms that compute all concurrent places in O`pP ` T qT P2˘ for live and bounded nets (where P and T are the numbers of places and transitions) and in O`PpP ` T q2˘ for live and bounded extended free-choice nets. Although these algorithms have a reasonably good computational complexity and are applicable to a large class of nets, large numbers of concurrent pairs of nodes may still lead to long computation times. This paper complements the palette of concurrency detection algorithms with the Concurrent Paths (CP) algorithm for sound (simple) free-choice workflow nets. The algorithm allows parallelization and has a worst-case computational complexity of OpP2 ` T 2q for acyclic nets and of OpP3 ` PT 2q for cyclic nets. Although the computational complexity of cyclic nets has not improved, the evaluation shows the benefits of CP, especially, if the net contains many nodes in concurrency relation.
Petr1i nets are a popular and well-studied notion to describe, investigate, revise, and analyze complex system behavior. Especially in the area of information systems and business process management, Petri nets are commonly used to model business processes. Instead of classical control-flow graphs resulting from procedural programming languages, nets are able to model concurrent behavior. Of course, although concurrency is an important aspect of nets (and the business process models they may represent), it complicates their analysis. The detection of concurrent places and transitions of nets helps to understand the behavior of a system. It further enables the measurement of similarity of nets with behavior [1], the derivation of other behavioral relations, such as e. g., causality, exclusivity [2, 3], etc. Some ongoing analysis, therefore, depends on concurrency detection and its efficiency.
Kovalyov [4] proposed a quintic time algorithm in the number of nodes that computes all concurrent places. Kovalyov and Esparza [5] revised that algorithm to obtain a time complexity of O`pP ` T qT P2˘ for live and bounded nets and of O`PpP ` T q2˘ for live and bounded extended free-choice nets (P is the number of places and T is the number of transitions of a net). Both algorithms are very general, well-suited, and efficient for their respective problem classes of nets. However, if a net contains many concurrent nodes, the computation time increases significantly during evaluation.
Decomposition of the net can be used to allow a parallel computation of the concurrency relation and to accelerate the computational method. A decomposition into single-entry single-exit (SESE) fragments helped to speed-up the computation in Weidlich et al. [6] and Ha and Prinz [7]. However, the SESE decomposition approach fails if the net contains inherently unstructured fragments (known as rigids). Weber et al. [8] proposed a quadratic time variant to compute concurrent nodes. Their algorithm requires a low number of nodes in the pre- and postset as well as only simple cycles (loops). For other cases, SESE decomposition and the approach of Weber et al. have to utilize the algorithm of Kovalyov and Esparza or more general techniques, such as state-space exploration or nfiite complete prefix unfolding [9]. Therefore, these approaches are again at least cubic in time complexity or worse for nets with arbitrary loops.
To overcome these limitations, this paper presents a new algorithm, called the Concurrent Paths (CP) algorithm, which is applicable to sound (simple) free-choice workflow nets . This class of nets is more restricted than those for the Kovalyov and Esparza algorithms, since it requires an explicit start and end place, 1-boundedness, and the simpler definition of free-choiceness [ 10, 11]. For acyclic nets, however, it has a quadratic worst-case computation complexity of OpP2 ` T 2q and, for cyclic nets, the worst-case complexity increases to a cubic algorithm of OpP3 ` PT 2q. The core idea of the approach is to consider concurrent paths instead of concurrent places and transitions. The CP algorithm is well parallelizable. In addition, the worst-case complexity occurs relatively infrequently, as it depends on the overall number of loops (incl. nested loops) in a net, which is usually small. If this number of loops can be interpreted as a constant, the complexity reduces to be quadratic in average. The restriction to connected workflow nets with single start and end places serves to introduce the method, but unconnected nets with several start and end places are also possible. In summary, the CP algorithm complements the palette of concurrency detection algorithms for the special case of sound (simple) free-choice workflow nets. A slightly extended version of this paper can be found as a technical report [12].
The remainder of the paper is structured as follows. Section 2 explains basic notions, especially nets, paths, loops, markings, and semantics. Subsequently, the concept of concurrency and the algorithm of Kovalyov and Esparza are introduced and described in Section 3. This is followed by revisions of their algorithm to the quadratic time CP algorithm for acyclic nets in Section 4. Section 5 extends the algorithm to the Concurrent Paths algorithm being able to handle cyclic nets. The evaluation in Section 6 demonstrates the strengths and weaknesses of the CP algorithm compared to the Kovalyov and Esparza algorithm for live and bounded free-choice nets. Finally, Section 7 summarizes the results and provides directions for future work.
This work is based on well-known definitions of Petri nets. Readers already familiar with these concepts may proceed directly to Section 2.3. However, a quick review is encouraged to ensure alignment with this paper’s specific notions.
Definition 1 (Petri net). A Petri net is a triple N “ pP, T, Fq with P and T are finite, disjoint sets of places and transitions and F Ď pP ˆ T q Y pT ˆ Pq is the flow relation. {
The union P Y T of a net N “ pP, T, Fq can be interpreted as nodes and F as edges between those nodes. For x P P Y T , ‚x “ tp | pp, xq P Fu is the preset of x (all directly preceding nodes) and x‚ “ ts | px, sq P Fu is the postset of x (all directly succeeding nodes). Each node in ‚x is an input of x and each node in x‚ is an output of x. The preset and postset of a set of nodes X Ď P Y T is defined as ‚X “ ŤxPX ‚x and X ‚ “ ŤxPX x‚, respectively.
Definition 2 (Path). A path W “ pn1, . . . , nmq of a net N “ pP, T, Fq is a sequence of nodes n1, . . . , nm P P Y T with m ě 1 and @i P t1, . . . , m ´ 1u : ni P ‚ni`1. {
Of course, places and transitions alternate on paths. Nodes are part of a path A “ px, . . . , yq, depicted x, . . . , y P A. If all nodes of a path are pairwise different, the path is acyclic; otherwise, it is cyclic. The acyclic path A is sometimes used as the set tx, . . . , yu. Pathspx, yq denotes the set of all acyclic
d f
D c g h
E i paths between nodes x and y, where x, y P P Y T . Two paths A “ px, . . . , yq and B “ py, . . . , zq can be concatenated to a new path A ` B “ px, . . . , yq ` py, . . . , zq “ px, . . . , y, . . . , zq. If A and B are acyclic and A X B “ tyu, then A ` B is acyclic since all nodes of A ` B are pairwise disjoint. A net N is cyclic if there is at least one node x P P Y T that has a non-trivial path (“ pxq) to itself.
Cyclic nets contain at least one loop. A loop is a subgraph of the net in which each node is reachable from any other node, which can be formally defined as follows: Definition 3 (Loop). A loop L “ pPL, TL, FLq of a net N “ pP, T, Fq is a strongly connected component of N, i. e., L is a maximal subgraph of N, such that PL Ď P, TL Ď T , and FL Ď F [13]. We denote the set of all loops of N with LoopspNq, such that LoopspNq “ H for acyclic nets. We further define EntriespLq as the set tl P pPL Y TLq : ‚l Ę pPL Y TLqu of loop entries of L, and ExitspLq as the set tl P pPL Y TLq : l‚ Ę pPL Y TLqu of loop exits of L. All flows in tpo, lq P F : o R pPL Y TLq ^ l P pPL Y TLqu are loop-entry flows and all flows in tpl, oq P F : l P pPL Y TLq ^ o R pPL Y TLqu are loop-exit flows of L. {
Each net in this paper is restricted to be (simple) free-choice: @p P P : |p‚| ą 1 ùñ ‚pp‚q “ tpu [10, 11]. Note that the free-choice property is usually used in its extended version: @t1,t2 P T : ‚t1 X ‚t2 “ H ùñ ‚t1 “ ‚t2 [14]. Polyvyanyy [10] and Favre et al. [11] provide bijective translations from nets belonging to the extended definition into nets applying to the simpler free-choice property, through the use of silent transitions. In the following, we use the terms free-choice to refer to the simpler and extended free-choice to refer to the extended definition.
Visualized nets have circles representing places, rectangles representing transitions, and directed edges representing flows (see Figure 1).
Definition 4 (Workflow and AFW-net) . A workflow net W N “ pP, T, F, i, oq is a net pP, T, Fq with i, o P P, ‚i “ H, and o‚ “ H. i is the source and o is the sink of W N. All nodes are on a path from i to o. If W N is free-choice, we call it FW-net. If W N is acyclic and free-choice, we call it AFW-net. { The visualized net in Figure 1 is a workflow (FW-)net as well as an AFW-net.
The state of a net is described by a so-called marking, which specifies the number of tokens in each place. Definition 5 (Marking). A marking of a net N “ pP, T, Fq is a total mapping M : P ÞÑ N0 that assigns a natural number (inclusively 0) of tokens to each place P. Mppq “ 1 means that place p P P carries 1 token in marking M. The mapping M is sometimes used as the set tp P P : Mppq ě 1u representing only places having at least one token in M. {
An initial marking of a net is a special marking with at least one place having a token. The initial
marking Mi of a workflow net W N “ pP, T, F, i, oq is a marking tiu where only the source i of a net
contains exactly one token. A terminal marking Mo is a marking tou of W N where only the sink o
contains exactly one token. Transitions whose input places all contain at least one token are enabled in a
marking and can be fired. This leads to the execution semantics of a net:
(
To simplify proofs in the remainder of this paper, we use the Path-to-End Theorem. The theorem states that in sound FW-nets, there is no reachable marking, in which at least two tokens are on an acyclic path to the sink.
Theorem 2 (Path-to-End Theorem). Let W N “ pP, T, F, i, oq be a FW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou.
Definition 6 (Execution semantics). Let N “ pP, T, Fq be a net with a marking M. A transition t P T is enabled in M iff every input place of t contains at least one token, @p P ‚t : Mppq ě 1. If t is enabled in M, then t can occur (“fire”), which leads to a step from M to M1 via t, denoted M Ñt M1, with #1, p P ‚t 0, else
#1, p P t‚ ` 0, else.
I. e., in a step via t, t “consumes” one token from all its input places and “produces” one token for all its output places [2]. {
Stepwise firings of transitions lead to chains of rfied transitions, which describe the behavior of a net as occurrence sequences: Definition 7 (Occurrence Sequences and Reachability). Let N “ pP, T, Fq be a net with a marking M0. A sequence of transitions σ “ xt1, . . . , tny, n P N0, t1, . . . , tn P T , is an occurrence sequence of M0 iff there is a sequence of markings M0, M1, . . . , Mn such that Mi´1 Ñti Mi holds for each i P t1, . . . , nu. It can be said that σ leads from M0 to Mn.
A marking M1 is reachable from a marking M (denoted MÑ˚M1) iff there is an occurrence sequence σ of M that leads to M1 or M “ M1. { Important properties of nets are liveness and boundedness: Definition 8 (Liveness and Boundedness). A net N “ pP, T, Fq with its initial marking M0 is live iff for every reachable marking M, M0Ñ˚M, and every t P T , there is a reachable marking M1, MÑ˚M1, which enables t.
N is n-bounded iff there exists a number n P N0 such that for every reachable marking M, M0Ñ˚M,
and for every place p P P it holds that the number of tokens at p is at most n: @p P P : Mppq ď n. N is
safe iff it is 1-bounded. {
Soundness describes an important property of workflow nets:
Definition 9 (Soundness). A workflow net W N “ pP, T, F, i, oq with its initial marking Mi “ tiu and its
terminal marking Mo “ tou is sound iff
(
@t P T DM, M1 : MiÑ˚M Ñt M1. [15] Theorem 1. Let W N “ pP, T, F, i, oq be a FW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou and W N “ `P, T Y tt1u, F Y tpo,t1q, pt1, iqu˘ be its “short-circuit” net.
W N is sound ðñ
W N is live and bounded
ÿ Proof. The preconditions by Theorem 2 are a FW-net W N “ pP, T, F, i, oq with its initial marking Mi “ tiu and its terminal marking Mo “ tou. The proof is done by contradiction. Let us assume that: Dp P P DW P Pathspp, oq DM, MiÑ˚M :
Mpwq ą 1
^
(
Following that path W is acyclic, w does not appear twice on W . As a consequence, there is at least one other input place w1 in ‚t X W , w “ w1, and, thus, |w‚| ą 1 and tw, w1u Ď ‚pw‚q “ ‚t.
Therefore, the FW-net W N is not simple free-choice.
(
Let w1, w2 P ‚t XW , w1 “ w2, be such two input places of t on path W with w1‚ “ w2‚ “ ttu. Since the sink has an empty postset, o‚ “ H, w1 and w2 cannot be o, w1 “ w2 “ o. By Def. 2 of paths, each node n P W (except the last node o on path W ) is directly followed by a node n1 P W X n‚ of n’s postset. For this reason and since w1 “ w2, w1, w2 P W , and w1‚ “ w2‚ “ ttu, w1 and w2 must directly be followed by t on path W . As a consequence, t appears at least twice on path W and, therefore, W ’s nodes are not pairwise different. This implies that path W is cyclic and not acyclic. Both cases fail. As a result, each transition t on W has exactly one input place on W , @t P W X T : |‚t X W | “ 1. In general, it is valid for W : ^ |t‚ X W | ě 1 As a consequence, firing a t P pW X T q in any marking M1 cannot reduce the number of tokens on W : ÿ Thus, the only possibility to reduce the number of tokens on W is a place pw P W X P with |pw‚| ě 2. Since |o‚| “ 0, pw “ o. As a consequence:
Dtt,t1u Ď pw‚ : t,t1 P T ^ t R W ^ t1 P W Let t,t1 be such transitions. Since W N is simple free-choice, it is valid for pw that ‚ppw‚q “ tpwu “ ‚t Y‚t1 and, therefore:
‚t “ ‚t1 “ tpwu
It results from (
A b e
B C d f
D
E
i c g h
Since W N is sound by (
A node x P P Y T is called active in a marking M, depicted as x˚M, in the following if it either contains a token (x P P and Mpxq ě 1) or is enabled in M (x P T, @p P ‚x : Mppq ě 1).
Definition 10 (Concurrency). For a given sound (simple) free-choice workflow net W N “ pP, T, F, i, oq
and its initial marking Mi “ tiu, there is a concurrency relation ∥Ď pP Y T q ˆ pP Y T q with px, yq P ∥,
x “ y, iff there is a reachable marking M, MiÑ˚M, with:
(
Kovalyov and Esparza [5] defined a cubic O`|P|p|P| ` |T |q2˘ algorithm to identify the ∥ relation for
live, bounded, and extended free-choice nets. We refer to the algorithm as the KovEs algorithm. The
KovEs algorithm is applicable to a wide range of net classes and is, therefore, more general than the
algorithm provided in this paper. In the remainder of this section, we provide an overview of its most
important concepts and explain its functionality. In doing this, we focus on KovEs in the context of sound,
simple free-choice workflow nets to revise the algorithm regarding this class of nets.
||
||
x
y
x
y
||
s
s
||
||
x
y
x
y
||
||
||
||
||
(a)
s
s
||
||
x
y
x
y
||
||
||
(b)
s
s
Case (
Case (
The initial step of the KovEs algorithm is based on a simple observation in free-choice workflow nets W N “ pP, T, F, i, oq with its initial marking M0 “ tiu: all places in the postset of transitions are pairwise in a concurrency relation (except for all reflexive pairs): `py, xq P ∥ ˘ For example, in Figure 2, the pairs tpb, eq, pe, bq, pc, dq, pd, cq, p f , hq, ph, f qu Ď∥. Besides transitions, all source places containing tokens in M0 can be handled in the same way: `py, xq P ∥ ˘
The KovEs algorithm extends an initial set of the concurrency relation R by considering each already
detected pair px, yq P ∥. Since px, yq P ∥, x (y) may also be concurrent to nodes in y‚ (x‚). For example,
pb,Cq is a new candidate for pb, eq in Figure 2. For x, this means that tpx, sq : s P y‚u are new candidate
pairs to be concurrent. For each candidate px, sq, there are exactly two cases: (
Consider case (
Considering case (
Algorithm 1 depicts the resulting algorithm of Kovalyov and Esparza [5]. It differs in its notation from the original in four ways: At first, it explicitly ignores reflexive pairs of nodes px, xq P pP Y T q ˆ pP Y T q; second, it uses the union-operator Ť for generating pairs to allow us a simpler discussion about its time complexity; third, line 9 is simplified to just E Ð R instead of E Ð R X `pP Y T q ˆ P˘ from the original paper since all pairs in R must fulfill the condition by lines 3 and 5; and, last, it uses the relation A as a mapping in lines 7 and 14 instead of a set.
Readers, who are not familiar with the algorithm, will find an explanation of the algorithm in the
following paragraph. Familiar readers may proceed directly to Section 4. In Algorithm 1, lines 3 and 5
determine the initial concurrency relations discussed as “initial step” above. Line 7 defines a mapping A
from each place to its directly succeeding places (i. e., the union of postsets of the postset of a place). This
is used in line 14 to quickly determine new pairs in relation. E in line 9 is a set that contains new pairs not
investigated yet. The while loop (lines 10–16) is iterated until E is empty. It takes an arbitrary pair px, pq
out of E (line 11) and one random transition t of the postset of p (line 12). Following case (
The KovEs algorithm has a worst-case time complexity of O`|P|p|P| ` |T |q2˘ resulting from its wide range of net classes for which it is applicable. This worst case appears if nets have a high level of concurrency, leading to long computation times as the evaluation will show later. This section revises the KovEs algorithm for AFW-nets based on soundness, the simpler free-choice property, and Observations 1 and 2 discussed in Section 3. An extension for cyclic FW-nets is presented in the next section.
The core idea of the revisions is to explore paths instead of directly succeeding nodes. As a consequence of the Path-to-End Theorem 2, a place cannot be in a concurrency relation with all places on all paths from this place to the sink. Therefore, for two concurrent places only those successors can be in a concurrency relation for which there is no path in-between. This core idea is investigated and refined in the following.
Concurrency of two different transitions in sound AFW-nets requires the absence of any path between them: Theorem 3. Let W N “ pP, T, F, i, oq be a sound AFW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou.
@x, y P P Y T, x “ y :
`Pathspx, yq Y Pathspy, xq˘ “ H
ùñ
px, yq R ∥
Proof. The precondition by Theorem 3 is a sound AFW-net W N “ pP, T, F, i, oq with its initial marking
Mi “ tiu and its terminal marking Mo “ tou. The proof is done by contradiction. We assume there is a
case, where x has a path to y or y has a path to x and both are still in a concurrency relation:
@x, y P P Y T, x “ y : `Pathspx, yq Y Pathspy, xq˘ “ H
^
Without loss of generality and following from this contradiction (
Pathspx, yq “ H ^
AxÑy P Pathspx, yq
Following from Def. 10 of concurrency, there is a marking M where x and y are active:
DM, MiÑ˚M : x˚M ^ yM
˚
To simplify ongoing considerations and following from (
#y, p P p‚x X Mq, x P T p P p‚y X Mq, y P T y P P Since x1 and y1 are places and W N is sound, Mpx1q “ Mpy1q “ 1. Furthermore, let Ax1Ñy1 be the modified path of AxÑy with adding x1 or removing y if necessary. Following from Def. 4, there is a path By1Ño from y1 to the sink o of W N: Since W N is acyclic by precondition:
Pathspy1, oq “ H ^
By1Ño P Pathspy1, oq Ax1Ñy1 ` By1Ño “ C ^
C is acyclic
As a consequence from (
Mpcq ě |tx1, y1u| “ 2
cPC XP
Since W N is sound, (
Following from Theorem 3 above, if two nodes are in concurrency relation, there is no path between
them.
{
(
C
E
A a b
F e
f Corollary 4. Let W N “ pP, T, F, i, oq be a sound AFW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou.
DM : MiÑ˚M ^ ˚ xM DM1 : M Ñy M1 ^ ˚ xM1 ^ ^ ˚ yM ùñ @x, y P P Y T, x “ y :
Pathspx, yq “ Pathspy, xq “ H Proof. The statement directly follows from the contraposition of Theorem 3.
For example, the AFW-net in Figure 2 has concurrent transitions B and C, pB,Cq P ∥, and concurrent places b and e, pb, eq P ∥. After firing transition C, Mp f q ě 1 and Mphq ě 1, such that pb, hq P ∥. As Cor. 4 states, there is neither a path from place b to e nor from place b to h. For place g, there is a path from place b to g; following Theorem 3, pb, gq R ∥. Regarding Cor. 4, each combination of two (different) concurrent active nodes cannot have any path in-between for sound AFW-nets.
Although the absence of paths between two nodes is a necessary condition for concurrency in AFWnets, it is not sufcfiient. For example, in Figure 4, place c has no path to place d, but both are never concurrent.
The existence or absence of paths between two nodes of an AFW-net is used in our approach to revise the KovEs algorithm. In doing this, we reconsider Observations 1 and 2 from Section 3. Recall that, given a pair of nodes px, yq P ∥ and a node s P y‚, we need to determine whether px, sq P ∥. Observation 1 with y P T states that @s P y‚, px, sq P ∥. Following Cor. 4, there cannot be a path from x to s: Corollary 5. Let W N “ pP, T, F, i, oq be a sound AFW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou. px, sq P ∥ Proof. Constructive proof for y P T , px, yq P ∥, s P y‚, and the initial marking Mi “ tiu and the terminal marking Mo “ tou. We prove both directions:
Pathspx, sq “ H ùñ px, sq P ∥: By Cor. 4 and since px, yq P ∥, there cannot be a path between x and y, Pathspx, yq “ H. Therefore, x R ‚y.
Following Def. 10 of concurrency and since px, yq P ∥, there is a marking M with x˚M and y˚M: { { (20) (21) Since y is active in M and y P T , y is enabled in M. As a consequence, firing y in M can lead to a marking M1 by Def. 6, in which s is active:
By Def. 10 of concurrency and since Pathspx, sq “ H and Pathspy, xq “ H by Cor. 4: px, sq P ∥. ✓ px, sq P ∥ ùñ Pathspx, sq “ H: By Cor. 4 and since px, sq P ∥: Pathspx, sq “ H. ✓ { (22) (23) (24) {
Observation 2 with y P P states that x is only concurrent to a transition s P y‚ if it is also concurrent to all places p in ‚s. This statement is complex to check but can be simplified by considering paths: Corollary 6. Let W N “ pP, T, F, i, oq be a sound AFW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou. px, sq P ∥ Proof. Constructive proof for px, yq P ∥, y P P, s P y‚, and the initial marking Mi “ tiu and the terminal marking Mo “ tou. Let
M, MiÑ˚M ^ ˚ xM ^ ˚ yM We prove both directions:
Pathspx, sq “ H ùñ px, sq P ∥: If x would have a path to any node in ‚s, it would have a path to s.
However, Pathspx, sq “ H. For this reason, x cannot have a path to any node in ‚s: As a consequence, since W N is sound, there must be a reachable marking M1, in which x is still active and s became enabled (active), i. e., firing s is “independent” from x, because there is no path from x to s by (23).:
DM1 : MÑ˚M1 px, sq P ∥ ùñ Pathspx, sq “ H: By Cor. 4 and since px, sq P ∥: Pathspx, sq “ H. ✓
In summary, for both cases y P P and y P T , if and only if x has no path to s, then px, sq P ∥. Otherwise, px, sq R ∥. This is summarized by the following theorem: Theorem 7. Let W N “ pP, T, F, i, oq be a sound AFW-net with its initial marking Mi “ tiu and its terminal marking Mo “ tou. px, sq P ∥ Proof. The theorem combines all cases from Cor. 5 and Cor. 6. ✓
Although this can already be used to revise the KovEs algorithm, we consider an additional revision as well.
Following the first revision, paths play a crucial role to identify concurrency. For this reason, we define an auxiliary relation: Definition 11 (HasPath relation). Let W N “ pP, T, F, i, oq be an AFW-net. The HasPath relation HasPath “ ␣px, yq P pP Y T q ˆ pP Y T q | Pathspx, yq “ H( (25) specifies whether a node x has an acyclic path to node y (HasPath is reflexive, so px, xq P HasPath). HasPathpxq denotes the set of all nodes to which x has a path (again, inclusive of itself). { x y || a b || ) x ( h t a P s a H ) y ( h t a P s a H x y || a || b c ) y ( h t a P s a
H
Case (a): Case (b):
HasPath(x)∩HasPath(y) = ∅ HasPath(x)∩HasPath(y) ≠ ∅
In the following, let px, yq P ∥ for a sound AFW-net. From px, yq P ∥ and Cor. 4 it follows that y R HasPathpxq and x R HasPathpyq. Let us consider any node a P HasPathpxq to which x has a path. If a would have a path to y (i. e., y P HasPathpaq), then x would have a path to y via a. For this reason, no node a P HasPathpxq has a path to y and no node in HasPathpyq has a path to x.
Regarding px, yq P ∥, there are exactly two cases: (a) No path starting in x to any sink crosses any path starting in y to any sink (i. e., HasPathpxq X HasPathpyq “ H, cf. Figure 5 Case (a)); or (b) at least one path starting in x to a sink crosses at least one path starting in y to a sink (i. e., HasPathpxq X HasPathpyq “ H, cf. Figure 5 Case (b)).
To case (a): each node in HasPathpxq must be in concurrency relation with any node in HasPathpyq after a stepwise application of Theorem 7 regarding the first revision (and, since tokens in both sets can never converge). This is illustrated in Figure 5 by nodes a and b being concurrent.
To case (b): the nodes of HasPathpxq are partially overlapping with the nodes of HasPathpyq. This y is illustrated in Figure 5 Case (b) with a gray triangle subset. Let Rx¯ “ HasPathpxqzHasPathpyq be the subset of nodes of HasPathpxq to which y has no path (and, therefore, no node in HasPathpyq as explained y ¯ previously). A node a P Rx has a subset HasPathpaq Ď HasPathpxq (illustrated as the grid triangle subset in Figure 5). Although no node in HasPathpyq has a path to a, a may have paths to nodes in HasPathpyq (more precisely, to nodes in HasPathpaq X HasPathpyq; in Figure 5 this is the subset of the gray triangle intersecting the grid triangle). Regarding Theorem 3, a cannot be concurrent to those nodes (c in the a ¯ illustration). Ry “ HasPathpyqzHasPathpaq contains all nodes of HasPathpyq to which a has no path (and so no other node of HasPathpaq). As a consequence, for each node a P Rxy¯, there are sets HasPathpaq and HasPathpyqzHasPathpaq “ Rya¯ being disjoint. There are disjoint paths from x to each node in HasPathpaq and from y to each node in Ra¯. Following the first revision and Theorem 7, a step-wise consideration of y these paths leads to concurrency between all nodes in HasPathpaq and Ra¯. Instead of considering these y nodes step-by-step, their pairwise concurrency can be added directly, i. e., HasPathpaq ˆ Rya¯ Ď ∥. This leads to a revised algorithm for sound AFW-nets with a quadratic computational complexity.
Algorithm 2 defines the revised algorithm for sound AFW-nets. The algorithm computes the concurrency relation for each node of the net. However, if necessary, it can be modified to just compute the relations for places. Furthermore, the algorithm assumes the relation ∥ to be represented as an adjacency list. Naturally, it takes just Op| ∥ |q to put it into a set of pairs.
Lines 2–6 of Algorithm 2 initialize the algorithm. Lines 3–5 initialize the set R for each unprocessed node with an empty set (following the KovEs algorithm, which is here the adjacency list of concurrent nodes). This initialization is linear to the number of nodes, Op|P| ` |T |q. Line 6 computes the HasPath relation as adjacency list by calling a function computeHasPath of Algorithm 3. The algorithm computes HasPath utilizing a reverse topological order (each node appears after all its output nodes). Such order Algorithm 3 Computation of HasPath as adjacency list for a given AFW-net W N “ pP, T, F, i, oq. 1: function COMPUTEHASPATH(W N “ pP, T, F, i, oq) 2: // Initialize 3: HasPath Ð H 4: for all x P P Y T do 5: HasPathpxq Ð H 6: L Ð P Y T in reverse topological order starting from o 7: for all x P L do 8: HasPathpxq Ð txu Y ŤsPx‚ HasPathpsq 9: return HasPath can be computed in Op|P| ` |T | ` |F|q [13]. Thus, Algorithm 3 can compute HasPath for all nodes in Op|P| ` |T | ` |F|q as well since each node (|P Y T |) is investigated with its outputs (|F|). Assuming that set operations (such as Y) can be achieved in constant time, e. g., with a BitSet, HasPath can be computed for all nodes in Op|P| ` |T | ` |F|q.
The actual computation of the concurrency relation takes place in lines 8–17. It creates a new adjacency list I for initial places in concurrency relation (line 8). It investigates all transitions t (line 9) and its output places x (line 10). Each x is initial concurrent to all other output places of t (line 11). Lines 12–13 investigate all pairs of different places being initially in concurrency relation in I. Line 14 computes the y ¯ set Rx containing all nodes to which x but not y has a path. As discussed in the Second Revision, each y node a P Rx¯ is investigated in lines 15–16, where line 16 adds all nodes in HasPathpyqzHasPathpaq to be concurrent to a (i. e., all nodes in HasPathpyq to which a does not have a path; recall that a does not have y ¯ a path to any node of HasPathpyq because it is in Rx).
The time complexity for lines 8–16 seems biquadratic, OpX 4q, at the first view. However, let us change the perspective on the algorithm focusing on line 16. If line 16 adds new information to Rpaq, at least one new pair in concurrency was detected. That means if line 16 always adds new information Rpaq and, therefore, finds a new pair in concurrency, lines 8–16 can execute line 16 at most | ∥ | ď |pP Y T q ˆ pP Y T q| times, i. e., Op|P|2 ` |T |2q — the algorithm would be quadratic. In other words, line 16 is never unnecessarily executed, as we will explain in the following.
The main task of lines 8–13 is to create and consider a new pair px, yq, which is taken from each t‚ of t in lines 8–11. There can only be |P|2 of such pairs (as adjacency list) in I. Apart from this pair (and, of course, py, xq), let us consider all other “initial” pairs pα, β q “ px, yq “ py, xq of lines 8–11. If for transition t with x, y P t‚ it is valid that t P HasPathpαq, then t‚ Ă HasPathpαq, and if it is valid that t P HasPathpβ q, then t‚ Ă HasPathpβ q. For this reason, it is valid that either: 1. tx, yu Ă HasPathpαq, 2. tx, yu Ă HasPathpβ q, or 3. tx, yu Ć `HasPathpαq Y HasPathpβ q˘.
As a consequence, all “initial” pairs px, yq and py, xq cannot be added by the handling of other “initial” y ¯ pairs. The same holds true for all nodes in Rx of line 14 whose information to be concurrent to y is firstly added in line 16. Line 16, therefore, always adds new information. As explained earlier, line 16 can at most be executed in quadratic complexity making lines 8–16 quadratic, Op|P|2 ` |T |2q.
In summary, assuming that set operations are applicable in constant time (like Y and z), e. g., by a BitSet, Algorithm 2 can be computed in O`p|P| ` |T |q ` p|P| ` |T | ` |F|q ` |P| ` |P|2 ` |T |2˘ “ O`3|P| ` 2|T | ` |F| ` |P|2 ` |T |2˘ “ Op|P|2 ` |T |2q in the worst-case (as |F| is quadratic to |P| ` |T | in the worst-case). Since at least those pairs in concurrency must be investigated, which are a subset of pP Y T q ˆ pP Y T q, it will be difficult to obtain a faster algorithm in terms of asymptotic time complexity than Op| ∥ |q Ď Op|P|2 ` |T |2q.
Although AFW-nets are not unusual, concurrency in cyclic sound FW-nets must be considered as well. In contrast to the KovEs algorithm, Algorithm 2 cannot be applied to cyclic nets since the revisions are applicable to acyclic nets only. To overcome this situation, we use a method called loop decomposition [17] to decompose a cyclic sound FW-net into a set of sound AFW-nets with the same behavior. Cyclic nets become acyclic by replacing loops with single loop places. Figure 6 shows a cyclic net on the left side, which is decomposed into four acyclic nets on the right side. Subsequently, we apply Algorithm 2 to each acyclic net and combine all collected concurrency information, i. e., all nodes concurrent to an inserted loop place are concurrent to all nodes in the corresponding loop.
The method of loop decomposition [17] was introduced to decompose sound workflow graphs with loops into sets of sound workflow graphs without loops. This decomposition method was slightly revised in [ 18]. Favre et al. [11] have shown how free-choice nets can be transferred into workflow graphs and vice versa. The notion of soundness used in the work of loop decomposition is equal to soundness of FW-nets [19]. For this reason, loop decomposition can be applied to sound FW-nets without strong modifications. Algorithm 4 describes the algorithm abstractly. The following only focuses on the consequences for concurrency detection. For further details about loop decomposition, we refer to previous work [17, 18].
Loop decomposition identifies loops as strongly connected components (cf. Def. 3 of loops). Following [17], entries and exits of loops are places in sound FW-nets. The (sometimes unconnected) subgraph between all loop entries and those loop exits being reachable without passing another loop exit is called the do-body of the loop. Once a loop exit contains a token, no other place in the loop or the do-body contains a token [17]. Therefore, the do-body can be interpreted as an implicit, initial “converging area” of different concurrent tokens before first loop exits are reached. Loop decomposition duplicates the do-body as an explicit, initial converging area before the loop. Subsequently, it replaces the entire loop (without the copied do-body) with a single loop place representing the previous loop. All flows into and out of the loop are redirected to start from and end at the loop place. Repeating this procedure with any (nested) loop finally leads to an acyclic sound FW-net [ 17]. For example, the cyclic network on the left Algorithm 4 Loop decomposition of a given sound FW-net W N “ pP, T, F, i, oq.
1: Connections Ð H 2: AcyclicNets Ð H 3: function DECOMPOSELOOPS(W N “ pP, T, F, i, oq) 4: Identify LoopspW Nq. 5: if |LoopspW Nq| “ 0 then 6: AcyclicNets Ð AcyclicNets Y tW Nu 7: return AcyclicNets, Connections 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: for all L “ pPL, TL, FLq P LoopspW Nq do
Identify loop entries EntriespLq and loop exits ExitspLq.
Identify do-body DoBodypLq of L.
Copy do-body and relink flows.
Replace L with place pL in W N and relink flows to pL.
Connections Ð Connections Y t`pL, PL Y TL˘u Split L into loop fragments.
Insert one source and one sink place to combine loop fragments.
Create new net W NL of it.
DECOMPOSELOOPS(W NL) DECOMPOSELOOPS(W N) return AcyclicNets, Connections in Figure 6 contains a loop with the nodes tb, B, c, d, C, e, D, f , E, Q, g, Fu at the top. This loop in turn contains a nested loop with the nodes tb, B, c, d, C, e, Q, g, Fu. However, this nested loop is only revealed when the surrounding loop is decomposed. Loop decomposition handles such loops recursively.
The extracted loops with all their nodes and flows are decomposed by removing all incoming flows of loop exits. As a consequence, the loop disintegrates into at least one loop fragment. In the original method of loop decomposition [17], each fragment is extended to an own net. This is unnecessary in this context of sound FW-nets, since all fragments of the same loop are mutually exclusive [17], i. e., no node of one fragment can ever be in a concurrency relation with a node of another fragment of the same loop. Therefore, all fragments of a loop together get a new single source place and a new single sink place. For each loop entry and exit, a new transition is inserted connecting the source place with the entry/exit. For each loop exit, a new transition is inserted to connect it with the new sink place. In addition, all transitions previously in the preset of a loop exit are connected to the new sink place. The resulting “loop” net is sound and free-choice. In case that this loop net is still cyclic (in case of nested loops), loop decomposition can be recursively applied to this net again. This procedure finally terminates in only sound AFW-nets [17].
Figure 6 illustrates the decomposition of the cyclic FW-net on the left into its set of AFW-nets. The cyclic net contains two loops: One with place b as entry and f as exit in the top and one with place h as entry and j and k as exits. The net is decomposed into four acyclic nets (right). The net at the top is the loop-reduced version of the cyclic net. The do-bodies (loop 1: tb, B, c, d,C, e, D, Q, g, Fu, loop 2: th, H, i, Iu) remained and the loops were replaced with loop places (α and β ). Since the remaining do-body of loop 1 contains a nested loop with loop entries b and g and loop exit e, the recursive decomposition replaces this loop with loop place γ and its do-body tb, B, c, d,Cu remains. The acyclic α-loop net corresponds to the upper loop place α and spans from before its loop exit f to before f (D). This net contains also the nested loop γ and is decomposed accordingly. The β -loop net corresponds to the lower loop place β . It consists of two fragments (from exit j to before k and from exit k to before j) and is constructed by adding a source place, sink place, and the remaining transitions. Finally, the γ-loop net represents the nested loop spanning from e to before e. F b
M n c d H L i l g Q
J
E B
C e
D f
R q a
A h
I j
O p
G
o K k
N m Sound cyclic FW-net b
B a
A h
H f k
E K c d g l i
C
The overall situation after loop decomposition is a set of sound AFW-nets, in which some loop places are linked to acyclic loop nets. It is important to understand for correctness that the replacement of (parts of) loops with loop places does not change the concurrency behavior. That is, in sound FW-nets, an entire loop (after copying the do-body) acts as a place “globally” [17]. For the computation of the concurrency relation it follows that each node in a concurrency relation with a loop place is concurrent with each node of the linked loop. Newly inserted transitions and places in the loop nets to facilitate the decomposition are not of interest, naturally. Nodes of loops in the do-body appear (at least) twice — once in the surrounding net and once in the corresponding loop net. For instance, places b and c in Figure 6 are in the AFW-net in the top and in the α-loop net. This does not have an influence on the final result, since if a node remaining in the surrounding net is in concurrency relation with another node, both nodes also are in concurrency relation in the original net. The same appears with nodes represented by the loop place being in concurrency relation with other nodes.
Algorithm 5 describes the Concurrent Paths (CP) algorithm. It computes the adjacency set R of concurrent nodes. This is initialized with an empty set in line 2. Line 3 calls Algorithm 4 to decompose net W N into a set of acyclic nets AcyclicNets and a Connections relation. Lines 4–5 compute (and extend) R for each acyclic net W Na with Algorithm 2. Lines 6–16 replace concurrency relations between loop places and other nodes. In doing this, it considers each connection between a loop place l and a linked loop net A (as combination of places and transitions) in line 6. For l, it considers each node c that is concurrent to l (line 7). If c is also a loop place with a linked loop net, the nodes of that loop net are assigned to B (lines 8–9). Otherwise, if c is an ordinary node, B only consists of tcu (line 11). Furthermore, although c is concurrent to the loop place l, it is not of interest since l is “virtual” (line 12). Then, each node a in A is concurrent to each node in B (lines 13–14). In addition, each node b in B is concurrent to each node in A (lines 15–16).
The time complexity of the algorithm depends on the time complexity of loop decomposition as well as on the (possible) increase of the problem size. Loop decomposition is achievable in Op|P|2 ` |P| ¨ |T | ` Algorithm 5 The Concurrent Paths (CP) algorithm: A cyclic version of the algorithm to determine ∥ for a sound FW-net W N “ pP, T, F, i, oq.
1: function CONCURRENTPATHS(W N “ pP, T, F, i, oq) 2: R Ð H 3: AcyclicNets, Connections Ð DECOMPOSELOOPS(W N) 4: for all W Na P AcyclicNets do 5: R Ð DETERMINECONCURRENCY(W Na, R) 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17:
else for all pl, Aq P Connections do for all c P Rplq do if c P Connections then
B Ð Connectionspcq X pP Y T q
B Ð tcu Rpcq Ð Rpcqztlu for all a P A do
Rpaq Ð Rpaq Y B for all b P B do
Rpbq Ð Rpbq Y A |P| ¨ |F|q [17, 18]. In the worst case of many nested loops, the problem size after loop decomposition may increase quadratically, i. e., instead of checking one net of size |P| ` |T | ` |F|, |P| nets of size |P| ` |T | ` |F| must be investigated as a result of the decomposition (in general, the number of (nested) loops in a net is limited by a low constant). Thus, the complexity of checking a single cyclic net may increase to Op|P|2 ` |T | ¨ |P| ` |P| ¨ |F|q in the worst case. In this worst case, the application of Algorithm 2 on |P| nets finally leads to a Op|P|3 ` |P| ¨ |T |2q and, therefore, cubic time complexity. For this reason, Algorithm 5 has the same time behavior as the KovEs algorithm in the worst case. Although it seems that Algorithm 5 has no benefit regarding the KovEs algorithm, there are several reasons why there are situations, in which the algorithm has its advantages: (i) The algorithm can be parallelized. At first, each resulting acyclic net can be analyzed in parallel.
The combination of the results is possible in at most quadratic time. At second, once HasPath is computed for a net in at most quadratic time, all transitions can be computed in parallel. The combination of the results is at most quadratic as well. (ii) It is relatively rare that nets have many (nested) loops [17]. In addition, if a loop has only one entry, it is not necessary to consider the do-body. The same holds true if the do-body does not contain any converging transition. (iii) If the net has a high degree of concurrency involving many nodes, the algorithm should have a performance benefit compared to KovEs.
(iv) Of course, if the net is acyclic, the algorithm is faster.
To illustrate how Algorithm 5 works, we use the cyclic example net of Figure 6. At first, loop decomposition decomposes the cyclic net into the acyclic nets on the right side of Figure 6. Subsequently, it performs for each of the acyclic nets the acyclic CP Algorithm 2. Table 1 contains the relation HasPath and the temporary relation R for each of the acyclic nets and most of their nodes. For example, if transition A is investigated, the pair pb, hq is considered. The sets HasPathpbq and HasPathphq can be found in Table 1. The table shows for each acyclic net and their nodes being illustrated in the top, the relations HasPath and R. For HasPath, we omitted the mention for nodes, which are not in concurrency relation with another node. Both relations were derived after performing Algorithm 2.
b
B a
A h
H c d i
C ⟲ γ
I c d i J
I C It is valid that HasPathpbqzHasPathphq “ tb, B, c, d,C, γ, D, α, R, qu. For each of these nodes, we can extend the relation to, e. g., Rpbq “ Rpbq Y `HasPathphqzHasPathpbq˘ “ Rpbq Y th, H, i, I, β , O, N, pu.
Once all acyclic nets are investigated, the results can be combined. For the upper acyclic net in Figure 6, there are three loop places α, β , and γ. Let us take α as an example: α is already concurrent to h, H, i, I, β , O, N, and p (cf. Table 1). Each of these nodes is considered by Algorithm 5, lines 7–16. It may start with node h, which is not a loop place but an ordinary node. Therefore, B Ð thu and h is not concurrent to α anymore (lines 10–12). However, each node in the α-loop net (Figure 6), is concurrent to h (lines 13–14); and h (in B) is concurrent to each node of the α-loop net. The same holds true for the case of β : It is a loop place so that B contains all nodes of the β -loop net (Figure 6), lines 8–9. That means, each node of the α-loop net is concurrent to each node of the β -loop net and, naturally, vice versa (lines 13–16). Table 2 summarizes the R (∥) relations for each node of the original net of Figure 6.
M n c d H
L Node
R (∥) a A b B c d C e D f E g F Q R q G
The nodes of the net in the top being in a concurrency relation ∥ after performing Algorithm 5 and combining B
C e
D f
R q a
A h
I j
O p
G o
The KovEs algorithm and the presented CP algorithm in Section 5 have been implemented in a simple script-based algorithm (PHP) for the purpose of evaluation. The implementation is open-source and available on GitHub1. The following experiments were conducted on a machine with an Intel® Core™ i7 CPU with 4 cores, 16 GB of main memory, and Microsoft Windows 11 Professional. PHP was used in version 8. We performed all measures for 10 times, removed the best and worst times, and used the mean values of all the remaining runs.
Both algorithms were applied to a well-known dataset, namely the IBM Websphere Business Modeler dataset [19], which consists of 1,368 files and is referred to as IBM hereafter. Only 644 nets of the IBM dataset can be investigated since the algorithm requires sound FW-nets. The nets were available as Petri Net Markup Language (PNML) models. The comparison of both algorithms was restricted to the identification of concurrent places instead of concurrent places and transitions, since the KovEs algorithm cannot find concurrent transitions without modifications. The nets under investigation are small (75% with less or equal 58 nodes) to big (with a maximum of 546 nodes). Places are more frequent than transitions (approx. 61%˘4% of all nodes are places). With regard to the number of nodes, a net has approx. 111%˘11.5% flows.
Both algorithms find the same places being concurrent for all suitable nets of the IBM dataset. Although the total number of nodes |N| in a net bounds the number of concurrent nodes | ∥ | ď |pP ` T q2|, the number of nodes (R2 “ 0.2), places (R2 “ 0.42), and transitions (R2 “ 0.06) do not well explain the Algorithm
KovEs CP 100,000 s e d o n 10,000 d e t a g itse 1,000 v n i. gLo 100
10 300,000 s e d no200,000 d e t a g i ts100,000 e v n I 0
0 degree of concurrency in a net by applying a linear regression considering whether | ∥ | „ |pP ` T q2|, | ∥ | „ |P2|, or | ∥ | „ |T 2|, respectively.
The overall goal was to construct a more efficient algorithm than the KovEs algorithm. For this reason, we have compared the times both algorithms need to compute all concurrency relations for a net. The CP algorithm was overall faster for the entire dataset. It just needs 285 [ms] to compute 192,170 pairs of places being in relation. On contrary, the KovEs algorithm requires 14,100 [ms] for doing the same job, i. e., the CP algorithm is approx. 50 times faster. On closer inspection, KovEs has its benefits for nets without a high degree of concurrency. For these cases, it performs better than CP. Figure 7 shows a chart comparing the number of investigated nodes during both algorithms in relation to the number of nodes in the net. The y-axis is scaled logarithmically. The CP algorithm has, of course, a higher “start up” number of nodes to investigate, because it visits at least each node and flow once for the computation of paths. KovEs instead directly starts with the computation of the concurrency relations and, therefore, has no start up number of nodes and has a better performance for nets with less concurrent nodes. Figure 8 illustrates the number of investigated nodes in relation to the number of relations. The chart reveals that the computational load of KovEs seems to increase slightly quadratically if the number of nodes in relation increase. Instead, the load of CP seems to increase only linearly for a higher number of relations. This correlation between the computational load and the number of relations becomes more obvious if we compare the computation time in relation to the number of nodes being concurrent as it is done in Figure 9. The computation time of the KovEs algorithm seems to increase quadratically to the number of concurrent nodes; instead, the computation time of CP seems to increase just linearly.
Only 40 out of 644 nets of the IBM dataset are cyclic. The acyclic nets are investigated in 241 [ms] with CP and in 14,084 [ms] with KovEs. In fact, one net with approx. 42k concurrent pairs alone needs 10,500 [ms] for KovEs but just 45 [ms] with CP. CP is faster than KovEs for 87 nets. In sum, CP needs 171 [ms] and KovEs needs 14,06 [ms] for these 87 nets (speedup factor approx. 82), whereas for the
Concurrent Paths
10.0
other 557 nets, CP needs 114 [ms] and KovEs needs 41 [ms] (slowdown factor approx. 3). The 87 nets
comprise approx. 172k of pairs in relation against approx. 20k for the others. Therefore, the 87 nets
have a much stronger computational intensity. KovEs is faster for the cyclic nets with 16 [ms] against 43
[ms] for CP. This is reasonable because of three reasons: (
Concurrency detection identifies pairs of nodes that may be executed in parallel. Knowing concurrent places and transitions in Petri nets is essential to understand their behavior and is crucial as the base for ongoing analysis. Since such nets are potentially large and complex with many pairs of concurrent nodes, efficient algorithms are necessary. This paper extends the palette of concurrency detection algorithms with the Concurrent Paths (CP) algorithm for sound and (simple) free-choice workflow nets. For acyclic nets, the algorithm performs in quadratic time OpP2 ` T 2q with P the number of places and T the number of transitions of a net. The algorithm requires a cubic time complexity in the worst-case for cyclic nets, OpP3 ` PT 2q. Although this seems not to be an improvement of the algorithm of Kovalyov and Esparza (KovEs) (which needs a cubic time complexity for live, bounded, and extended free-choice nets and, therefore, a wider range of net classes), parallelizing CP is straight-forward and the worst-case of CP appears significantly less frequent than the worst-case of KovEs and can be assumed to have just a constant impact on computation time for most nets. An evaluation of CP on a benchmark of nets showed strong benefits on nets with a high degree of concurrency and only small disadvantages on nets with a low degree of concurrency.
This paper enables Petri net analysis to be more efcfiient, especially, in cases of a high degree in concurrency of nets. Although single nets could be analyzed efficiently with KovEs, performing concurrency detection on a large set of nets (e.g., for indexing in a database) may require much time. CP reduces the effort and enables more efcfiient strategies to compute other properties of nets such as causality, exclusivity, etc. As a side effect, related research areas such as business process management and information systems research profit from the new technique as they utilize nets for analysis.
For future work, we plan to apply CP to efficiently derive all relations in the 4C spectrum [ 2] for sound free-choice workflow nets. This would allow for an efficient indexing of nets in querying languages for nets, which is especially beneficial in business process management.