In this paper, we sketch a data-centric approach to avoid deadlocks of a business process. If dependencies between data values are neglected or modelled incorrectly, this can lead to errors in the control flow of the business process. We address the problem of detecting deadlocks which are caused by the improper handling of data. We show by example, how these deadlocks can be detected by means of a symbolic reachability graph. Under certain conditions, we can derive the correct dependency between the involved data values. This allows to modify the business process in a way so that the detected deadlocks will not be reachable.
The design of business processes is an error prone task. This motivates the use of
formal verification to help a business process designer to avoid certain kinds of
errors. Models of business processes can be transformed into more formal models
like process algebra [
However, little attention has been paid to the influence of data on the
correctness of a business process. Most formal models represent data only in a highly
abstracted and imprecise form. Models that explicitly include data usually have
a clear separation between the control flow part and the data part [
In this paper, we consider processes that are heavily influenced by data and
might be unable to finish a task for some combinations of data values. Technically,
this means that a deadlock is reachable under some conditions. Our goal is to
find out those harmful combinations of data values and describe the relation
the value must adhere to in order to avoid a deadlock (e. g. in the form of a
function) and use this information to fix the process. Concerning this aspect,
our approach is more general than the approach of [
We represent a business process by a High-Level Petri net [
start x id(x)
y order
id exp. prod.
receive [x=y] x stop y product id-1(y) manufacture start x id(x)
y order
id exp. prod.
receive [x=y] x stop y product z manufacture customer manufacturer customer manufacturer (a) Correct business process (b) Incorrect business process
Consider a business process formed by a customer and a manufacturer (Fig. 1a). The customer orders a product x from the manufacturer by telling the manufacturer the product’s id (order). The manufacturer assembles the product associated with the id and returns the product to the customer (manufacture). Let us now assume that due to a design error in the manufacturer’s internal workflow, the id y obtained from the customer is lost and replaced by the id of an arbitrary product z (Fig. 1b). Then, the customer will get a product different from the one he expects. In that case, no further action (receive) can be performed because the condition x = y is not satisfied and we reach a deadlock. We call this a conditional deadlock, because it occurs only if the compared data values are not equal. Note that in a more complex scenario, a choice dependent on data may not always lead to a deadlock instantly but later on in the process. In that case, the deadlock condition has to be propagated backwards. This aspect will not be covered in this paper.
We introduce an approach to detect conditional deadlocks and to derive the dependency between values that must be used in order to avoid the deadlock. In Sect. 2, we illustrate by simple examples, how to identify deadlocks by means of a symbolic reachability graph. Section 3 shows by a more sophisticated example, how to derive the precise conditions under which an conditional deadlock can be avoided. It is not always possible to derive these conditions precisely. Section 4 shows an example that can not be corrected with our approach due to imprecise results. In Sect.5, we conclude our work. 2
In this section, we show how to detect a deadlock by means of the symbolic reachability graph (SRG) of the Petri net. In the following examples, we assume that every place has the type integer except for some places that carry tokens (denoted as black dots) that do not have a value. A marking m of a Petri net N is considered a deadlock, if no transition is enabled and m is not contained in a set Ω of final markings of N .
In each of the following exam- p0 p0 ples, we assume that the net is in a final marking exactly when the t0 t0 [x 0] npelatcNe1pΩin Fisigm.a2ark.eWd.e Ccaonnseiadseilry tsheee p1 xx [ p0t]0 <x=V0> p1 xx that N1 is not deadlock free and t1 [x 0] [ p1=V0 ] t1 [x 0] M = {[p1 = n]|n ∈ Z, n < 0} is x t1 <x=V0> x the set of deadlocks reachable in pΩ [ pΩ=V0, V0 0 ] pΩ N1. Obviously, by adding the guard (a) N1 (b) SRG(N1) (c) N10 x ≥ 0 to t0, we can ensure that t1 will always be enabled and N1 will Fig. 2: Net with a conditional deadlock and eventually reach the final marking its correction [pΩ] (Fig. 2c).
In a marking of the symbolic reachability graph, every value is represented by a term. Without going into technical details, we show how to construct the symbolic reachability graph of N1. Starting from initial marking [p0], t1 produces an arbitrary integer on p1 (Fig. 2b). We represent this integer by a unique identifier V0. Thus we get the marking [p1 = V0]. While formally V0 is a constant, we treat V0 as a variable: V0 may later be instantiated by any value from Z. Since t1 is enabled only if V0 is non-negative, we keep the condition in V0 ≥ 0 in the successor marking [p2 = V0, V0 ≥ 0] of [p1 = V0] (we obtain the condition by combining the firing mode of t1 and the guard of t1). We consider an instance of a marking of the symbolic reachability graph valid, if every condition denoted in the marking evaluates to true. Obviously, a marking of N1 is reachable exactly if it is a valid instance of a marking of the symbolic reachability graph.
With the symbolic reachability graph, we can identify under which condition a marking instantiates to a deadlock. Here, [p1 = V0] is a conditional deadlock for ¬V0 ≥ 0 since each instance of [p1 = V0] has no successor for this condition. We now enforce that the condition V0 ≥ 0 holds in [p1 = V0] by adding the guard x ≥ 0 to the predecessor-transition t0 of [p1 = V0]. We obtain a corrected version N10 of N1, which is deadlock free.
t0 x x x p0 p1 pΩ (a) N2 x x x
t2 [x<0] t1 t3 [x>0] t0 <x=V0> [ p1=V0 ] [ p0 ] t2 <x=V1> [ p1=V1 ] t1 <x=V0> t3 <x=V0> t1 <x=V1> t3 <x=V1> [ pΩ=V0, V0<0 ] [ pΩ=V0, V0>0 ] [ pΩ=V1, V1<0 ] [ pΩ=V1, V1>0 ]
(b) SRG(N2)
Fig. 3a shows a net N2 which is not deadlock free and which has a branching symbolic reachability graph. Note that the values produced by t0 and t2 obtain different identifiers (although both branches behave symmetrically). [p1 = V0] and [p1 = V1] are conditional deadlocks of N2. [p1 = V0] is a deadlock for ¬((V0 < 0) ∨ (V0 > 0)). Any successor of an instance of [p1 = V0] belongs either to the branch with condition V0 < 0 or the branch with condition V0 > 0. We enforce the condition (V0 < 0) ∨ (V0 > 0) by adding the guard (x < 0) ∨ (x > 0) to t0 (which is effectively equivalent to x 6= 0). By repeating this procedure for [p1 = V1], we get the same guard for t2 and obtain a deadlock free net. 3
In the previous section, we have shown that by adding an appropriate guard, we can prevent the reachability of deadlocks. Adding a guard or replacing a guard by a more restrictive one makes the net less permissive, that is the set of reachable markings gets smaller. Naturally, we want to prevent all deadlocks from being reachable. On the other hand, we do not want to prevent the reachability of more markings than necessary. This section addresses the issue of deriving a least restrictive guard. How to derive a guard (like x > 0) from a condition (like V0 > 0) is not obvious if more than one variable is involved and functions are used in the arc inscriptions.
Without loss of generality, we assume that the symbolic reachability graph is a tree (if not, we can unfold it). Note that the symbolic reachability graph usually has an acyclic structure since names of value identifiers never repeat. In the tree, we always modify the guard of the transition that directly precedes the deadlock. It should be mentioned here, that due to restrictions inherent to the modelled the business process (e. g. the dependency on of external events which can not be influenced), it might not be possible to modify that transition. In that case, we choose the first modifiable predecessor transition in the tree. As guard derivation is more involved in that case, it will not be shown here. Consider the net N3 in Fig. 4a, which reaches a deadlock if the integer produced by t1 on p3 is greater than the integer produced by t0 on p1. An ad-hoc way to fix N3 is to add the guard z ≥ y to t1. Then, N3 eventually reaches the final marking [pΩ]. However, the guard z ≥ y − 1 would also ensure that N3 reaches [pΩ] but is less restrictive than x ≥ y, since it evaluates to true for more assignments of x and y. The guard y = 6 ∨ z ≥ y − 1 is even less restrictive than z ≥ y − 1.
We derive this guard from the symbolic reachability graph in Fig. 4b. m0 is a deadlock for condition ¬(V0 ≤ V1) since ev- p0 ery valid instance of m00 satisrfieeaschVa0bi≤lityV1o.f Wme0 upnrdeverenctonthdei- p1 xt0 p2[xx≠+51] tion ¬(V0 ≤ V1) by adding a y guard to t1. It is sufficient that t1 [ p0 ] the guard forbids the violation of x z t0 <x=V0> V0 ≤ V1 only for valid instances p3 [ p1=V0, p2=V0+1, V0≠5 ] (=m) of m and m0. So we can assume z t1 <y=V0+1,z=V1> that for a step m →a m0 (where t2 [x z] [ p1=V0, p3=V1, V0≠5 ] (=m’) iant=egte1rhsy V=0 Va0n+d V1,1zg=iveVn1i) with pΩ [ pΩ, V0≠5t,2V<0z=VV11]> (=m’’) (1) the condition V0 6= 5 already (a) N3 (b) SRG(N3) holds (precondition in m) Fig. 4: A net that is less obvious to correct (2) y and z are bound to the valuations of V0 + 1 and V1 (firing mode of t1).
This motivates the definition of the expression
∀V0, V1 ∈ Z : V0 6= 5 ∧ y = V0 + 1 ∧ z = V1 =⇒ V0 ≤ V1 We call this expression least restrictive V0 ≤ V1-enforcing (for step m →a m0). Note that the more preconditions an expression has, the less restrictive it is. V0 and V1 are all-quantified because the condition V0 ≤ V1 shall be enforced for any valid instance of m0. It is easy to see that this expression is indeed equivalent to y = 6 ∨ z ≥ y − 1. Since V0, V1 are uniquely determined by y and z, we can replace V0 by y − 1 and V1 by z, thus eliminating V0, V1 from the expression.
We go back to the business process introduced in Fig. 1a. The reader may believe that there is a deadlock m0 = [exp. prod. = V0, product = V1] for condition ¬(V0 = V1) which is reachable from m = [exp. prod. = V0, id(V0)] via transition manufacture. This leads to the expression ∀V0, V1 ∈ Z : y = id(V0) ∧ z = V1 =⇒ V0 = V1, which is equivalent to z = id−1(y). Thus we have reconstructed the dependency between products and their id’s and may correct the business process by replacing z by id−1(y).
In general, several successive deadlock elimination steps are necessary in
order to obtain a deadlock free net, as every step may introduce new deadlocks.
Our approach is similar to Dijkstra’s method to derive the weakest precondition
for which a given program terminates in a specified state [
Note that modifying a transition may have non-local side-effects if the transition appears more than once in the tree. In that case, more markings are rendered unreachable than intended, leading to a suboptimal solution. As the next section shows that even without non-local side-effects, it is not always possible to get an optimal solution. 4
Some nets can not be corrected using the expression derived in the last section. Consider the net N4 in Fig. 5a. There is no unique way to avoid the deadlocks of p0 t0 p1 t1 p2 [x<y] t2 pΩ py
px x y y x (a) N4 [ p0 ]
t0 <x=V0> [ p1, px=V0 ]
t1 <y=V1> [ p2, px=V0, py=V1 ]
t2 <x=V0, y=V1> [ pΩ, V0<V1 ] (b) SRG(N4) N4. For example, we get a deadlock free net N40 (Fig. 5c) by adding the guard x < 5 to t0 and y ≥ 5 to t1. However, instead of 5, we could have chosen any other integer. The symbolic reachability graph does not give us a hint on how to derive the general structure of the two guards. Here, the expression enforcing V0 < V1 for m t1hy=V1i m0 (with m = [p2 = V0, p1], m0 = [p2 = V0, p3 = V1]) gives →
∀V0, V1 ∈ Z : y = V1 =⇒ V0 < V1 which evaluates to false for every y ∈ Z. The expression is too restrictive due to a lack of information. The condition V0 ≤ V1 that shall be enforced depends on both the values of V0 and V1, but t1 has no access to the place px on which V1 is stored. For the slightly different net N400 (Fig. 5d) in which t1 has access to both values, an appropriate guard for t1 can be derived: The expression enforcing V0 < V1 gives ∀V0, V1 ∈ Z : x = V0 ∧ y = V1 =⇒ V0 < V1, which is equivalent to x < y.
A related phenomenon is known from controller synthesis. A controller forbids
the supervised system to perform some actions in certain situations. The guards
we add to a transition have an impact on the net comparable to a controller.
If certain sets of states are indistinguishable for the controller, then there is
no unique maximal permissive controller [
The detection and correction of errors in a business process is a tedious task. Petri nets provide of formal foundation to apply formal verification on business processes. We have shown how to identify and avoid deadlocks of a High-Level Petri net by means of a symbolic reachability graph. As a byproduct, our approach allows to formulate the dependencies between data values that must hold in order to avoid a deadlock.
Our goal is to apply our approach in a distributed setting. Therefore, several problems have to be considered. Since one part of a business process usually does not have complete information about the state of the other parts, problems caused by a lack of information as described in Sect. 4 are more likely to occur. It is also less likely that a deadlock can be fixed locally. Especially in the presence of cycles, non-local side-effects occur inevitably.
In contrast to [