Control-flow analysis of business process models requires to check the absence of lack of synchronization. We use workflow graphs, which may contain inclusive OR gateways, to represent the control-flow of business process models. We structurally characterize lack of synchronization in an acyclic workflow graph. Based on this characterization, we show how to detect lack of synchronization in quadratic time.
A business process model can be simulated, used for automated code generation,
or directly executed by a workflow engine. With the increasing popularity of
these use cases, ensuring that a process is free of control-flow errors is essential.
A process is sound [
In this paper, we show how to efficiently check the absence of lack of
synchronization in acyclic workflow graphs with IOR gateways. In Section 3, we show
that a lack of synchronization in acyclic workflow graphs with IOR gateways can
be fully characterized in term of a path with a handle. In Section 4, we show how
to detect a path with a handle by using an extension of the approach of Perl and
Shiloach [
Related work: In case a workflow graph does not contain IOR gateways, it can
be easily converted into a Petri net and vice versa [
We use number of known concepts from set theory, graph theory, and the workflow graph verification which are defined below:
Let U be a set. A multi-set over U is a mapping m : U → N. We write m[e] instead of m(e). For two multi-sets m1, m2, and each x ∈ U , we have : (m1 + m2)[x] = m1[x] + m2[x] and (m1 − m2)[x] = m1[x] − m2[x]. By abuse of notation, we sometimes use a set X ⊆ U in a multi-set context by setting X[x] = 1 iff x ∈ X and X[x] = 0 otherwise.
A directed graph G = (N, E) consists of a set N of nodes and a set E of ordered pairs (s, t) of nodes, written s → t. A directed multi-graph G = (N, E, c) consists of a set N of nodes, a set E of edges and a mapping c : E → (N ∪ {null}) × (N ∪ {null}) that maps each edge to an ordered pair of nodes or null values. If c maps e ∈ E to an ordered pair (s, t) ∈ N , then s is called the source of e, t is called the target of e, e is an outgoing edge of s, and e is an incoming edge of t. If s = null, then we say that e has no source. If t = null, then we say that e has no target. For a node n ∈ N , the set of incoming edges of n is denoted by ◦n. The set of outgoing edges of n is denoted n◦. If n has only one incoming edge e, ◦n denotes e (◦n would denote {e}). If n has only one outgoing edge e′, n◦ denotes e′.
A path p = hx0, ..., xni from an element x0 to an element xn in a graph G = (N, E, c) is an alternating sequence of elements xi in N and in E such that, for any element xi ∈ E with c(xi) = (si, ti), if i 6= 0 then si = xi−1 and if i 6= n then ti = xi+1. If x is an element of a path p we say that p contains x. A path is trivial, when it is contains only one element. A cycle is a path b = hx0 . . . xni such that x0 = xn and b is not trivial. If there exists a path from an element x1 to an element x2 of a graph, we say that x1 precedes x2, denoted x1 < x2.
A workflow graph W = (N, E, c, l) consists of a multi-graph G = (N, E, c) and a mapping l : N → {AN D, XOR, IOR} that associates a logic with every node n ∈ N , such that: 1. An edge with null as source is a source of the workflow graph and an edge with null as target is a sink of the workflow graph. 2. The workflow graph has one source and at least one sink. 3. For each node n ∈ N , there exists a path from the source to one of the sinks that contains n. W is cyclic if there exists a cycle in W .
Let, in the rest of this section, W = (N, E, c, l) be an acyclic workflow graph.
c a e itso,kseTinmhieglaasmrelmye.atIonftPincesthroaifsnweAtoNsr,kDdfleolfiwongeigcdr,aaepsxheas- s D F d J f M h cuting n removes one token from each b t of the incoming edges of n and adds S g O one token to each of the outgoing edges of n. If n has XOR logic, executing n Fig. 1. A workflow graph . removes one token from one of the incoming edges of n and adds one token to one of the outgoing edges of n. If n has IOR logic, n can be executed if and only if at least one of its incoming edges is marked and there is no marked edge that precedes a non marked incoming edge of n. When n executes, it removes one token from each of its marked incoming edge and adds one token to a nonempty subset of its outgoing edges. The outgoing edge or set of outgoing edges to which a token is added when executing a node with XOR or IOR logic is nondeterministic, by which we abstract from data-based or event-based decisions in the process model. In the following, this semantics is defined formally.
A marking, m : E → N, of a workflow graph with edges E is a multi-set over E. When m[e] = k, we say that the edge e is marked with k tokens in m. When m[e] > 0, we say that the edge e is marked. The initial marking ms of W is such that the source edge s is marked by one token in ms and no edge, other than s, is marked in ms.
Let m and m′ be two markings of W . A tuple (E1, n, E2) is called transition if n ∈ N , E1 ⊆ ◦n, and E2 ⊆ n◦. A transition (E1, n, E2) is enabled in a marking m iff for each edge e ∈ E1 we have m[e] > 0 and any of the following proposition: – l(n) = AN D, E1 = ◦n, and E2 = n◦. – l(n) = XOR, there exists an edge e such that E1 = {e}, and there exists an edge e′ such that E2 = {e′}. – l(n) = IOR, E1 and E2 are not empty, E1 = {e ∈ ◦n | m(e) > 0}, and, for every edge e ∈ ◦n \ E1, there exists no edge e′, marked in m, such that e′ < e.
A transition T can be executed in a marking m iff T is enabled in m. When T is executed in m, a marking m′ results such that m′ = m − E1 + E2.
An execution sequence of W is an alternate sequence σ = hm0, T0, m1, T1...i of markings mi of W and transitions Ti = (Ei, ni, Ei′) such that, for each i ≥ 0, Ti is enabled in mi and mi+1 results from the execution of Ti in mi. An execution of W is an execution sequence σ = hm0, ..., mni of W such that n > 0, m0 = ms and there is no transition enabled in mn. As the transition between two markings can be easily deduced, we often omit the transitions when representing an execution or an execution sequence, i.e., we write them as sequence of markings.
Let m be a marking of W , m is reachable from a marking m′ of W iff there exists an execution sequence σ = hm0, ..., mni of W such that m0 = m′ and m = mn. The marking m is a reachable marking of W iff m is reachable from ms.
A lack of synchronization is a reachable marking m of W such that there exists an edge e ∈ E that carries more than one token in m. 3
To characterize the lack of synchronization, we follow the intuition that potentially concurrent paths, i.e., paths starting with an IOR-split or an AND-split, should not be joined by XOR-join. In the following, we formalize this characterization and show that such structure always leads to lack of synchronization in deadlocks free acyclic workflow graphs.
Definition 1 (Path with a AND-XOR or a IOR-XOR handle). Let p1 = hn0, ..., nii and p2 = hn′0, ..., n′ji be two paths in a workflow graph W = (N, E, c, l).
The paths p1 and p2 form a path with a handle1 iff p1 is not trivial, p1 ∩p2 = {n0, ni}, n0 = n′0, and ni = n′j. We say that p1 and p2 form a path with an handle from n0 to ni. The paths p1 and p2 form a path with a AND-XOR handle iff they form a path with a handle, n0 is an AND-split, and ni is an XOR-join. The paths p1 and p2 form a path with a IOR-XOR handle iff they form a path with a handle, n0 is an IOR-split, and ni is an XOR-join. In the rest of this document, we use handle instead of path with a AND-XOR handle or path with a IOR-XOR handle. The node n0 is the start node of the handle and the node ni is the end node of the handle. 1 Strictly speaking, one path is the handle of the other path and vice versa. Theorem 1. In an acyclic workflow graph that contains no deadlock, there is a lack of synchronization iff there is a handle.
The outline of the only if direction of the proof of Theorem 1 is that, whenever there is a handle, this handle can be ‘executed’ in the sense that there exists an execution such that a token reaches the incoming edge of the start node of the handle and then two tokens can be propagated to reach two incoming edges of the end node of the handle to create a lack of synchronization. We believe that, due to its direct relationship with an erroneous execution, the handle is an adequate error message for the process modeler. Note that it is necessary that the workflow graph is deadlocks free in order to show that the handle can be executed and thus a lack of synchronization be observed. However, even if the workflow graph contains a deadlock, a handle is a design error because, once the deadlock is fixed, the handle can be executed and a lack of synchronization can be observed. 4
Given an acyclic directed graph G = (N, E) and four different nodes s1, s2, t1, t2 ∈
N , Perl and Shiloach [
Our intuitive view of the approach proposed by Perl and Shiloach [
In the remainder of the this section, we describe how to obtain a line graph: a directed graph in which the edges are represented as nodes. Based on the line graph and a numbering allowing us to detect which edge is upstream from another, we show how to build the state graph. Finally, we describe how to detect handles using the state graph.
Computing a line graph: Perl and Shiloach [
For the purpose of checking handles, there are two types of nodes that are of interest: 1. The start nodes of a possible handle S = {x | x ∈ N ∧ x is an AND-split or an IOR-split}. 2. The end nodes of a possible handle T = {x | x ∈ N ∧ x is an XOR-join}. We include these nodes in the line graph. s a
F b c d I e f
M g
In the following, for any edge e of a directed graph t(e) references the target node of e and s(e) references the source node of e.
Definition 2 (Line graph). Let W = (N, E, c, l) be an acyclic workflow graph. The line graph L = (N ′, E′) of W is a directed graph such that:
N ′ = E ∪ S ∪ T E′ = {a → b | a, b ∈ E ∧ t(a) = s(b)}
∪ {a → b | a, b ∈ N ′ ∧ ( (a ∈ S ∪ T ∧ a = s(b)) ∨ (b ∈ S ∪ T ∧ t(a) = b) )}
Generating the state graph: We build a state graph from the line graph of
an acyclic workflow graph. Each node of the state graph is a multi-set containing
two nodes of the line graph, i.e., two edges of the original workflow graph. Such
multi-set represents a state of the line graph where the two nodes carry a token.
The edges of the state graph represent the allowed token moves. In order to
determine which node of the line graph is upstream of another, i.e., to determine
the allowed token moves, we compute a value v(n) given by the reverse post
order numbering of the nodes [
Definition 3 (State graph). A state graph of an acyclic simple directed graph L = (N ′, E′) is an acyclic directed graph F = (N ′′, E′′) such that: N ′′ = {[x, y] | x, y ∈ N ∧ x 6= y} ∪ {[x, x] | x ∈ S ∪ T }
E′′ = {[x, y] → [x′, y] | x → x′ ∈ E′ ∧ v(x) ≤ v(y)}
Figure 3 shows the state graph of the line graph of Figure 2. As shown by
Perl and Shiloach [
Checking for handles: In order to detect the existence of a handle in the original workflow graph, we have to check if there exists a path in the state graph from a state with two tokens on a node in S to a state with two tokens on a node in T . This is achieved by traversing the graph from each unvisited node in S until reaching a node in t ∈ T or having visited all the reachable nodes. In the worst case, the graph traversal visits each node of the graph once. The edges that belong to the handle in the workflow graph can be easily retrieved: They are the edges that are on the path from the state with two tokens on a node s ∈ S to the state with two tokens on a node t ∈ T of the handle in the state graph. On Figure 3 we observe that there is a path between [I, I] and [O, O] which indicates that there is an handle between I and O in workflow graph of Figure 1. 5
We propose an intuitive structural characterization for lack of synchronization in acyclic workflow graphs that contain inclusive OR logic: the handle. The handle is an adequate error message to the process modeler. We show how to check for handles by building a state graph. The size of the state graph is quadratic with respect to the original graph. All other operations are linear either with respect to the size of the original graph or the state graph. Thus, our approach requires quadratic time and space to check for handles. Note that the approach can be easily adapted to detect potential concurrency between two elements of the process. This has multiple applications. For example, we can detect two tasks accessing concurrently the same data store.