=Paper=
{{Paper
|id=None
|storemode=property
|title=Sound Recoveries of Structural Workflows with Synchronization
|pdfUrl=https://ceur-ws.org/Vol-1032/paper-07.pdf
|volume=Vol-1032
|dblpUrl=https://dblp.org/rec/conf/csp/Chrzastowski-WachtelGL13
}}
==Sound Recoveries of Structural Workflows with Synchronization==
https://ceur-ws.org/Vol-1032/paper-07.pdf
Sound Recoveries of Structural Workflows with
Synchronization
Piotr Chrza̧stowski-Wachtel, Pawel Gola̧b, and Bartosz Lewiński
Institute of Informatics, Warsaw University,
Banacha 2, PL 02-097 Warszawa, Poland
pch@mimuw.edu.pl, pawel.golab@mimuw.edu.pl, bartosz.lewinski@mimuw.edu.pl
Abstract. We consider communication places in workflow nets, where
the connected transitions lie in parallel threads. When a workflow Petri
net is constructed structurally, by means of refinements, such places can-
not be modeled structurally. They are added after the net is constructed.
Workflow nets constructed in a structural manner are sound, but addition
of such communication places can result in losing the desired soundness
property. However, there is a method to avoid such misplacement of com-
munication places. We should limit the pairs of connected transitions to
the ones that lie in truly parallel threads and to avoid cycles introduced
by communication places.
Recovery transitions — special kind of transitions used as a powerful
tool in dynamic workflow modeling — allow the manager to move to-
kens arbitrarily, when some unexpected situation happens. They were
extensively studied and proved to be a useful tool in the workflow man-
agement [HA00]. They can be modeled as a kind of reset transitions with
additional feature of depositing tokens taken from a specified region to
particular places in this region, like it was proposed in [Ch06]. Mov-
ing tokens arbitrarily by the manager requires a lot of attention, since
soundness of the net can easily be destroyed. In this paper we present a
sufficient and necessary condition of soundness for a marking in a struc-
tured net with communication places. Verifying the condition turns out
to be fast. The cost is linear with respect to the total number of places
and transitions.
1 Introduction
Workflow management is an area, where workflow designers can prove correct-
ness and flexibility of their models. It has been studied in numerous papers,
like [WS09], [BPS09]. One of the major problems is how to organize commu-
nication between parallel tasks performed by communicating agents [BPM05].
Making communication pattern wrongly can easily lead to deadlocks, mutual
waiting or leaving messages as trash, when they are deposited somewhere, and
not consumed by anyone. The danger of bad design increases, when we talk
about management that lasts in time and needs rearrangement due to some
unexpected situations.
74 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
Composing workflow nets in a structural way was proposed in [ChBHO03]. A
number of basic node refinement rules has been introduced. These rules include
sequential split, parallel split, choice and loop splits. They reflect typical pro-
gramming constructs like sequence of actions, an invocation of parallel threads,
instruction of choice and a loop statement. The control of the workflow runs can
be hence guarded by these constructs. Restricting the nets to the nets obtained
from a single node by these structural constructs was proven in to guarantee
soundness, as defined by [vdAtH00].
As it was already recognized in [ChBHO03], these constructs are not sufficient
for typical needs of a workflow designer. In the cited paper a number of non-
structural synchronization rules were proposed. By non-structural we mean here
adding of new nodes and edges, which do not result as a refinement of existing
nodes. Among them the most important was the synchronization of two parallel
actions. When in two parallel threads A and B we want an action b from B to
wait until an action a from A has been executed, we can model it by introducing
a new communication place s with arcs leading from a to s and from s to b. Such
construct we call a synchronization or communication, depending on whether we
emphasize the fact that b must wait for a or that a has something important
to communicate to b. Introducing such synchronization places can result in a
possible deadlock or other unsound constructs, like trash tokens generation. In
order to avoid misintroduction of such places, a criterion was proposed, which
is a sufficient condition for soundness. The condition was based on the idea of
the refinement tree, reflecting the history of refinements. It has been proven that
refinement trees are unique up to an isomorphism for a given structural WF-
net. In other words, if a WF-net is constructed structurally, then all the histories
creating this net differ only in unimportant details (like the order of refinements
in disjoint areas), resulting in the same refinement tree.
p1
t1 t2
p1 p9
p2 p3 p6 t8
t3 t4 t6 p8
t1 t5 t2 t9
p4 p5 p7 t7
t5 t9
p9 p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8
Fig. 1. Example WF -net and an corresponding refinement tree
Sound Recoveries of Structural Workflows with Synchronization 75
In dynamical workflows it is often desired that the control is being changed
during the lifetime of the workflow execution. Such situations are quite normal,
especially when workflows describe processes that last for a long time (months
or even years). Sometimes the manager decides to detour from the anticipated
control flow and would like to “correct” the flow manually moving tokens around.
Situations of this kind can happen in particular, when for instance under some
time pressure we decide to skip several actions or when we decide that some part
of the workflow should be repeated due to unexpected failures, which were not
foreseen during the design. In such cases we would like to support the workflow
management by allowing the manager to perform only sound rearrangements of
the flow. When no such restriction would be set, the manager, quite possibly
without understanding side effects, could make undesirable changes. This can
lead to unwanted behavior, making the net unsound.
One of the main problems with such on-the-fly changes of the markings is
to determine the impact area, which is the least part of the net, called region,
which is affected by the rearrangement of tokens. The refinement tree gives us
precise information — in order to define the impact area caused by any changes
in the net, it suffices to find the latest common predecessor of the nodes, where
the changes were made. The nodes which are not descendants of this node are
not affected by these changes.
The changes we consider are of two kinds. First of them is the addition
of places or transitions in an unstructured manner. An example of such useful
addition is the introduction of a place joining two transitions, which are in (dif-
ferent) parallel threads. If such a place connects transition t with transition r,
then the intention is to suspend the execution of r until t is executed. Clearly the
introduction of such a place can result in a deadlock. In [ChBHO03] a strong suf-
ficient condition was presented guaranteeing net soundness after such insertion
of a communication place. It turns out that if an inserted place connects such
two transittion-type leaves t and r in the refinement tree that no choice-split or
loop-split node is found on the path from t to r and if no cycle can be detected
in the net after such insertion, then the resulting net is sound.
The second kind of change is of dynamical matter. We allow the manager to
modify the marking by arbitrary moving tokens around some region. A region is
understood as the net unfolded from a single place-type node in the refinement
tree. Inside a region we consider the so-called recovery transitions, which remove
tokens from the whole area and restore them in arbitrarily chosen places. Our
goal is to find conditions, which would protect the manager from depositing
tokens on such places, that the resulting marking would be unsound, hence not
properly terminating.
2 Refinement Rules
This section is a short reminder of WF -nets refinement rules introduced in
[ChBHO03]. The idea behind is that having defined the refinement rules preserv-
ing certain network properties, we are able to analyse WF -networks that were
76 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
p1
t1 t2 p1 p9
p2 p3 p6 t8
t3 t4 t6 p8
s t1 t5 t2 t9
p4 p5 p7 t7
t5 t9
p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8
p9 s
Fig. 2. Example of net synchronization with corresponding refinement tree
constructed by using those rules. To construct such network one starts with a
single place, and then repeatedly applies context-free rules on network elements.
One of biggest advantages of using refinement rules approach is construction
trace called refinement tree that contains much information about the network
structure. An example of such tree and corresponding network can be found on
figure 1. The rest of this section covers basic rules presented in [ChBHO03]. All
described rules are depicted on figure 3.
The first two rules are called sequential splits. They are used to create linear
sequence of places and transitions, like p2 → t3 → p4 on figure 1. It’s an example
of splitting a single place. There are two kinds of sequential splits depending
on the node type they are applied to. We call them sequential place split and
sequential transition split respectively. Splits of this type introduce partial order
of transitions in sound transition firing sequences. Splits replace the chosen node
with three other nodes: the first and the last are of the same type and have either
the same inputs or outputs as the original node, respectively. The third node is
the one in the middle that connects two other nodes, so is of opposite type.
The next two rules are equivalent to logical AN D and OR gates respectively.
The first of them applies to places and the second one to transitions and both
are replacing node with two copies of it.
The first split called parallel split introduces two parallel threads that will be
executed simultaneously. In sound transition firing sequences transitions from
different parallel paths can be safely swapped (if partial order defined by other
splits is preserved). Examples of such paths are p2 → t3 → p4 and p3 → t4 → p5
on figure 1.
The second split, called choice split, defines two alternative paths that the
process can follow. During a single process run, transitions of only one of the
Sound Recoveries of Structural Workflows with Synchronization 77
Fig. 3. Basic WF -nets refinement rules. Starting from top: sequential place split, se-
quential transition split, parallel split, choice split and loop split.
paths can be enabled. Examples of such paths are t1 → . . . → t5 and t2 → . . . →
t9 on figure 1.
The last split type introduces loops and therefore is called a loop split. A
loop example with nodes later splitted by sequential split rules can be found on
figure 1.
3 Definitions
In this section we’ll present some definitions and notation conventions that will
be used in the rest of the article.
Siblings. For the node v that is a child of sequential split type node p, let
right siblings be defined as siblings that occur after v in p’s children order. The
definition of left siblings of v is analogous.
78 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
Prenodes. We define Prenodes (v) set as follows. Let pi be the i-th node on
the path from root to v. Then for each pi of sequential split type, Prenodes (v)
includes pi , left siblings of pi+1 and their subtrees.
This definition corresponds to the original refinement tree, without using
additional edges provided by synchronisations.
Existential marking function. Below we present notation and definition for ex-
istential marking function which returns information if in a given set of nodes
any places are marked.
(
? 0 if M (v) = 0 for each v ∈ V
M (V ) =
1 otherwise
Structured SWF -net (Synchronised WorkFlow network) is an extension of
WF -net defined as a 7-tuple hP, T, F, s, e, S, Ci, where
1. hP, T, F, s, ei is a standard structured WF -net with the set of places P ,
transitions T , flow function F the source place s, and the exit place e.
2. S — the set of synchronisation places (semaphores)
3. C — the set of edges joining semaphores and synchronised transitions. It is
easy to see that C ∩ F = ∅
When two transitions t1 and t2 are synchronised via place s, we denote
t1 as in(s) and t2 as out(s).
4 Soundness Characterisation
The main goal of this chapter is to find properties of marking M in SWF -net
that guarantee soundness. Before introducing these properties we’ll define two
auxiliary sets Before and After, that will help us in those properties formulation
and we’ll explore some important properties of them.
4.1 Before and After sets
Intuitively, Before (v) and After (v) sets include places and transitions, that are
over or under vertex v in WF -net graph respectively. In the case of SWF -nets
we consider only such nodes that are not synchronisation places during Before
and After sets construction.
We define Before (v) set as follows. A leaf l is in Before (v) if and only if there
exists a predecessor q of l being a left-sibling of some node lying on the path
from the root to v inclusively. Similarly for Af ter(v) we consider right siblings
instead. We ignore the synchronisation places.
An important feature of Before and After sets is that Before (v) and After (v)
sets are not containing v itself, so immediate conclusion from Before and After
sets definitions is that Before (v) ∩ After (v) = ∅ for each node v.
Sound Recoveries of Structural Workflows with Synchronization 79
It is worth to explore, how Before and After sets are constructed in the case
of loops. We can distinguish two cases depending on whether loop contains the
node for which these sets are constructed or not.
Let us consider loops from the first case. Let l be the loop that was created
by splitting place pl and transition tl . In this case Before and After sets will
either contain leaves only from pl subtree or only from tl subtree.
In the second case the Before and After sets can either contain all the leaves
of the given loop or none of its nodes.
In the forthcoming text it is important to have clarity about Before and After
sets containment rules. Let v, vb , va be the vertices such that vb ∈ Before (v) and
va ∈ After (v). Clearly, Before (vb ) ⊂ Before (v) and After (va ) ⊂ After (v). We
also have v ∈ After (vb ) and v ∈ Before (va ). And so, finally, After (v) ⊂ After (vb )
and Before (v) ⊂ Before (va ).
The Before and After sets have some interesting properties in the context of
sound marking, that we will formulate in the following proposition. We say that
a node (place or transition) x in a Petri net is reachable from a given marking
M if it is not dead in the case x is a transition or it can be marked by some
marking reachable from M , in the case x is a place.
Proposition 1 Let M be a sound marking of WF-net with synchronisations.
For each place or transition x we have:
1. M (x) ≥ 1 implies M (After (x)) = 0
2. M (Before (x)) > 0 implies M (After (x)) = 0
3. M (Before (x)) > 0 implies M (x) = 0 and x is reachable.
Proof. Let hP, T, F, s, e, S, Ci be a structured SWF -net and M a sound marking
on this network.
We begin the proof with some observations. When constructing the Before
and After sets, we take into account only subtrees related with nodes that are of
sequential split type. The sequential split type nodes determine the partial order
of transitions in possible transition sequences transforming any sound marking
M (in particular M1s ) into M1e . Some transitions are incomparable in this order
because of different types of nodes, for example AN D nodes that introduce
concurrency in nets. This partial order results in important properties of Before
and After sets.
For a transition t ∈ T that is not a part of any loop, the set After (t) con-
tains all transitions that can fire after t occurs in a sequence transforming a
sound marking M into M1e and that this firing is directly dependent on t. If the
transition t is in a loop, the same condition holds, except for some other transi-
tions from this loop — not all of them are included in After (t) set. But still, all
transitions from the loop that belong to the After (t) set in order to fire, need
transition t to fire before them.
It is important to stress out here, that we only consider transition sequences
that contain t when writing about firing dependences. In the case of transitions
that come after AN D nodes, there are at least two independent paths which
can lead to those transitions firing, so there are possible situations, when t won’t
80 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
occur in such sequences but the considered transitions will still fire. Neverthe-
less, if t occurs in such a sequence, it determines the path that the process went
through and we know that t firing is necessary in order to make the next transi-
tions firings possible. We have a similar situation in the case when t results from
loop main transition fragmentation (as t7 and t8 on figure 1).
With this observation, we can move to the main part of the proof.
1. The first step is a direct result of our observation. If x = e then this point
is obvious. If x 6= e then M (x) ≥ 1 means that x is a place and x is an input for
some transitions Tx ⊂ T .
Firstly, let’s consider nets that contain no loops. Each transition in any se-
quence transforming M1s into M can occur only once. Since x isn’t empty, we
know that none of the Tx transitions will occur in possible transition sequences
transforming M1s into M. Taking into account our observation this also means
that none of the transitions from After sets of Tx transitions will occur in such
sequences. It means that none of outputs of Tx transitions or outputs of transi-
tions from their After sets is marked. We also know, that all the transitions from
Tx , all their outputs and their After sets are in After (x). Moreover it is easy to
find that these are the only items in After (x). So we have M (After (x)) = 0.
The case of loops is very similar. The only problem is that x can be a loop
element. It is possible in this case, that not all of Tx transitions will be in After (x)
set — some of them can be transitions starting new loop iteration. However, it
is easy to recognize that this makes no problem, and reasoning for transitions
from Tx that are in After (x) is still valid.
2. This property is a simple consequence of 1. We know that for all places from
Before (x) that marking M is greater than zero and their After sets markings
is zero too. We also know that After (x) set is a subset of those After sets, so
M (After (n)) = 0.
3. First part of this property is also a consequence of point 1. We know, that
for all places from Before (x) for which the marking M is greater than zero, their
After sets markings equal zero. We also know that x is an element of those places
After sets, so M (x) = 0.
The fact that x is reachable is a result of our observation. Let ty be such a
transition that is in After set of some place from Before (x) that the marking M
is greater than zero, and for which this place in an input. We know that x is in
ty ’s After set, so there exists a transition tx for which x is an output and either
tx ∈ After (ty ) or simply tx = ty . Because marking M is sound, it is possible for
ty to fire. In the case when tx 6= ty , we know from the observation and from the
fact that the marking M is sound [ChBHO03], that it is also possible for tx to
fire, so x is reachable.
4.2 Properties of sound SWF -net markings
In this section we’ll give a characterisation of SWF -net sound markings in the
form of a short lemma. Before formulating the lemma, it is worth noticing, that
as in the case of standard WF -nets, if M is a sound marking of WF -net with
synchronisations, then M is 1-bounded (there can’t be two tokens at a one place).
Sound Recoveries of Structural Workflows with Synchronization 81
Lemma 1 Let N = hP, T, F, f, ei be an WF-net and Ns = P, T, F, f, e, {s}, C
be the same net with added synchronisation place s. Given Ns marking M is
sound if and only if:
1. M|N is sound in N
2. Exactly one of following holds:
(a) M (Before (in(s))) > 0
(b) s is marked
(c) M (After (out(s))) > 0
(d) Synchronisation was skipped, so M (Before (in(s)) ∪ After (in(s))) = 0
and M (Before (out(s)) ∪ After (out(s))) = 0
Basically, the lemma describes intuitions about how synchronisation place
should work. It says, that we have four different states, that our process can be
in. First three cases are straightforward: it can be either before synchronisation,
during synchronisation or after synchronisation. The last one is the case, when
the synchronisation occurs in one of the branches that resulted from an choice
split, and an active branch is not the synchronised one. An example of such
situation is depicted below on figure 4.
p1
t1 t2
p2 p3 p6 t8
t3 t4 t6 p8
s
p4 p5 p7 t7
t5 t9
p9
Fig. 4. Example of synchronisation skipping marking
Therefore, for the sake of precision, we can describe the first three states
as: synchronisation place is active, process is during synchronisation and syn-
chronisation is inactive, but either synchronisation has occurred, or the process
branch without synchronisation is at the evaluation point, when marked places
are in After (out(s)) set. The last one describes situation when process finished
considered fragment with alternative). Nevertheless it is more convenient to use
definitions presented in the previous paragraph.
82 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
To show that the above intuitions are right, we will now prove our lemma.
Proof. It is important to remember that synchronization of items in loops is not
allowed, so in every valid transition sequence in(s) and out(s) can occur only
once.
Firstly let us assume that a marking M is sound in Ns = P, T, F, f, e, {s}, C
net.
What synchronisation point does, is prohibiting certain transition sequences
that allow obtaining marking M|N from M1s in N , by enforcing firings of one tran-
sition group before another. It is important that synchronisation is not adding
any new possible transition sequences. This means, that any transition sequence
that leads to the marking M in Ns is also valid in N , leading to the marking
M|N . This means that M|N is sound in N , so 1. holds.
For the case when there exists such OR place that allows to skip synchroni-
sation, let pin be the place before such fork, and pout first place after it. From
the rules of synchronization we know that in this case pin is in Before (in(s))
and pout is in After (out(s)).
It is easy to see, that each of the conditions a), b) and c) exclude d) and vice
versa. Now we’ll show that a), b) and c) exclude each other. If M (Before (in(s))) >
0, then we know from the proven proposition, that there is no transition sequence
that leads to a marking M containing in(s), so s will be empty for each valid
subsequence of those transitions, which means that there was no possibility for
out(s) to fire, so again from the proposition, M (After (out(s))) = 0.
If s is marked, than in(s) has already fired. We know that M |N is valid
so, Before (in(s)) marking must be empty. Again from the proposition we have
M (After (out(s))) = 0, because there was no possibility for out(s) to fire.
If M (After (out(s))) > 0 then it means that transitions in(s) and out(s) have
already fired, so s is empty and from the validity of M|N , either M (Before (in(s)))
is empty or the process was run following a path where no synchronisation occurs.
In the second case we have M (pout ∪ After (pout )) > 0, we have that M (s) = 0
and M (Before (in(s))) = 0, because M (pin ∪ Before (pin )) = 0 according to the
proposition.
If none of the conditions a), b) or c) holds, we have M (Before (in(s))) = 0,
M (s) = 0 and M (After (out(s))) = 0. There are two possibilities. Firstly, we
may consider situation when M (After (in(s))) > 0 and M (Before (out(s))) > 0,
but in this case s can’t be empty, because it would make impossible for out(s)
to fire and we know from the proposition that it has to fire in order to clean up
tokens from Before (out(s)).
The only valid option is M (After (in(s))) = 0 and M (Before (out(s))) = 0,
which means that all tokens are in After (pin ) ∩ Before (pout ) on process path
disjoint with the synchronisation. There are no other options because of the
synchronisation rules, which allow to synchronize only these transitions, which
are not separated by choice or loop split nodes in the refinement tree. So we
know now that a), b), c) and d) exclude each other and in each case one of them
must hold, so soundness of Ns means that 1. and 2. hold.
Now lets assume that 1. and 2. from the lemma hold.
Sound Recoveries of Structural Workflows with Synchronization 83
M|N is sound, so let hxi i be a sequence of events leading to M1e in N . It’s
easy to see, that in case when one of b), c) or d) holds, the same sequence can
be fired in Ns . In the case when s is not empty, this sequence will clean s. A bit
harder is the case when a) holds, but one can easily see, that it is possible to
rearrange hxi i so that in(s) will occur before out(s) and still all transitions from
Before (in(s)) will be before in(s) and all transitions from After (out(s)) will be
after out(s). Rules of synchronisation guarantee that such operations will lead
to valid transition sequence, which will also be valid in Ns and will lead to the
same result as the original sequence.
This proves that if 1. and 2. from the lemma hold for a given marking M
that the marking is sound.
We have proved implications in both directions, so the lemma is valid.
5 Soundness Checking
The algorithm for checking the soundness of a marking will be a modification
of the soundness checking algorithm (theorem) from presented in previous work
[Ch06].
As a reminder, two functions w and W were defined as follows:
1 if v = root
w(parent (v))
if v is a child of a node which is not a parallel
w(v) = split node
w0 (parent(v))
c if v is a child of a node of the parallel split node,
with c children
M
(v) w0 (v) for each place-leaf v
P
W (v) = y∈Ch(v) W (y) for all internal nodes x
0 for each transition-leaf t
The theorem stated that a marking is sound if and only if for each tree node
x either W s (w)(x) = 0 or W s (w)(x) = w(s). We will now define new functions
ws , W s and S such that W s and S will have the same signature as W and
ws will have the same signature as w. Note that the values in W and S are
determined only by leaves — for the internal nodes we take sum of the values of
their children. For both in(s) and out(s), we will add additional weight to the
path from the node to the root, and propagate this change downwards for the
pre-nodes (nodes occurring to the left of it). Let cs be a constant such that for
every node x the condition w(x) > cs is satisfied.
We will apply the following transformation two times to W presented in
[Ch06] for both in(s), out(s), with c equal to cs , −cs respectively.
For every node v on the path from t to root we add the weight c
w0 (v) = w(v) + c
84 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
For every node v ∈ Prenode (in(s)) (nodes on the left of the path from in(s)
to root)
1
if v = root
ws (parent (v)) if v is a child of a node which is not a parallel
ws (v) = split node
ws (parent(v))
if v is a child of a node being a parallel split
c
node, with c children
For the remaining nodes ws (v) = w(v). The function W remains unchanged,
except for the fact that now it depends on ws .
?
cs · (M (s) + M (After (out(s))))
if t = in(s)
S(M )(t) = −cs · (M? (After (out(s)))) if t = out(s)
0 for every other case
We will use this transformation two times to nodes in(s), out(s) with c being
inverses of each other. Notice that this pair of transformations together changes
nodes only inside the smallest subtree containing them.
p1 1 p1 1
t1 1 t2 1 t1 1 t2 1
p2 3/4 p3 1/4 p6 t8 1 p2 3/4 p3 1/4 p6 t8 1
1 1
+1/4 t3 t4 -1/4 t6 1 p8 1 +1/4 t3 t4 -1/4 t6 1 p8 1
s s
1/4 1/4
p4 1/2 p5 1/2 p7 t7 1 p4 1/2 p5 1/2 p7 t7 1
1 1
t5 1 t9 1 t5 1 t9 1
p9 1 p9 1
Fig. 5. Example of SWF -net with marked weights defined by functions from the the-
orem. The marking on the left is sound, while the marking on the right isn’t, which
results in weight explosion in t1.
Theorem 1 A marking M of the SWF-net N is sound if and only if for each
s s
node v in the refinement tree either WM (v) + S(v) = w(v) or WM (v) = 0
Sound Recoveries of Structural Workflows with Synchronization 85
Proof. We will prove it by using the sound characterisation lemma.
Let M be a sound marking. By the above lemma, exactly one of following
holds:
1. M (Before (in(s))) > 0
2. s is marked.
3. M (After (out(s))) > 0
4. Synchronisation was skipped, so M (After (in(s)) ∪ Before (in(s))) = 0 and
M (Bef ore(out(s) = 0) ∪ After (out(s)))
p1 p9
t1 t5 t2 t9
p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8
s
Fig. 6. Derivation Tree with paths highlighted
Lets reason case by case, we will prove that in each of these cases our algo-
rithm will correctly verify the marking:
1. If M (Before (in(s))) > 0: Both in(s) and out(s) are inactive (which means
S(in(s)) = S(out(s)) = 0). The marking M is sound, so M (After (out(s))) = 0
and M (After (in(s))) = 0. This means that all the marked nodes are in modified
left sides (“Before”) of trees, so the verification behaves just as in the W without
synchronisation, because all the weights were just decreased by some amount.
2. If synchronization place s is marked: in(s) is active and out(s) is inactive.
Since M(After (in(s)) ∪ Before (in(s))) > 0 and M (Before (in(s))) = 0, we have
M (After (in(s))) > 0 and because the marking is sound, it meets S(in(s)) in
some node in the path to root, and then S(in) modifies it to the correct amount
86 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński
3. If M (After (out(s))) > 0: both in(s) and out(s) are active. Of course in this
situation M(After (in(s)) ∪ Before (in(s))) > 0 and M (Before (in(s))) = 0, so we
have M (After (in(s)))) > 0 The marking is sound, so it meets the S(in(s) in some
node in the path to root, and then S(in(s)) modifies it to the correct amount.
Similarly, since M (After (out(s))) > 0 and marking is sound, the verification
succeeds until it meets at the path from in to root and here it is corrected by S
from in(s)
4. If synchronisation was skipped, so M (After (in(s)) ∪ Before (in(s))) = 0
and M (Bef ore(out(s) = 0) ∪ After (out(s))): The modifications to weights we
made apply only to nodes in the path from in(s) to out(s) and they are all
empty in this case.
This proves that in every case, our verification succeeds.
Let us prove the opposite implication now. Let M be such a marking that for
s s
each node v in the refinement tree either WM (v) + S(v) = w(v) or WM (v) = 0.
We will show that the cases from the lemma are exclusive:
1. excludes (2. or 3.) Let’s assume M (Before (in(s))) > 0. Then if 2. or 3.
then in(s) is active, but since M (Before (in(s))) > 0, there is an active node
that is on the left hand side from the path from in(s) to root, but it was already
modified by c, so when S will meets, there will be c added two times.
2. and 3. Easy case, W (in(s)) = ws (in(s)) · M (s) + M? (After (out(s))) =
2ws (in(s)) > ws (in(s))
It is easy to see that 4. is disjoint from the other cases too. We need only
to distinguish 4. from 2.: If M (s) > 0 then W (in(s)) > 0, and since 4. holds,
W (out(s)) = 0, so in the place where paths from in(s) to root and out(s) to root
meet there will be an unbalance.
Hence the cases from the lemma are disjoint. We need to prove now that
at least one of them holds. Let’s assume none of them holds. Then in(s) and
out(s) are not active. Assume that M (Before (out(s))) isn’t empty. Because of
1., M (Before (in(s))) = 0, so there are nodes enabled to the right from the path
from out(s) to the root node, that are below least common ancestor of in(s)
and out(s). When the weight of those active nodes gets passed to the path, they
s
need S to have WM (v) + S(v) = w(v), but in(s) is inactive, so we came to a
contradiction.
Similarly, assume M (After (in(s))) > 0. Because of 1., M (After (out(s))) = 0,
so there are enabled nodes to the left from path from out(s) to the root node, that
are below least common ancestor of in(s) and out(s). When the weight of those
s
enabled nodes get passed to the path, they need S to have WM (v)+S(v) = w(v),
but in(s) is disabled, so we came to a contradiction.
These two arguments imply that 4., M (After (in(s)) ∪ Before (in(s))) = 0
and M (Bef ore(out(s) = 0) ∪ After (out(s))), so at least one of the cases from
the lemma holds.
Now we need to prove the first part of the lemma, that M|N is sound in N .
The proof of this fact is identical to first part of this proof. We show that if one
of 1., 2. or 3. occurs, the rest of checking behaves identical to checking done in w.
Sound Recoveries of Structural Workflows with Synchronization 87
6 Conclusion
We have proven that the important construction of creating a channel between
two transitions (like links in BPEL4WS) can be done in a semi-structured man-
ner with the preservation of soundness. We have discovered a condition that
is sufficient and necessary for a marking to preserve soundness. The condition,
based on the structure of the refinement tree is fast to verify; in fact it is linear
with respect to the number of nodes of the net (so even better than the size
of the net: the edges, with possible quadratic number of them, do not count).
This condition allows us to determine soundness of an arbitrary marking and
allow on-the fly changes of markings during the execution of a workflow. Such
changes are considered a powerful tool for a manager to change a marking in
an arbitrary manner in case of an unexpected detour from the normal workflow
run. Support by automatic verification, if such changes can cause an undesired
behavior (like deadlock or creation of trash tokens) is an important improvement
of the technology.
References
[vdAtH00] W.M.P.van der Aalst, A.H.M. ter Hofstede, Verification of Workflow Task
Structures: A Petri-net-based Approach, Information Systems, 25(1): 43-69, March
2000.
[ChBHO03] Piotr Chrza̧stowski-Wachtel, Boualem Benatallah, Rachid Hamadi, Mil-
ton O’Dell, Adi Susanto, Top-down Petri Net Based Approach to Dynamic Workflow
Modelling, Lecture Note in Computer Science. v2678. 336-353., 2003.
[Ch06] P.Chrza̧stowski-Wachtel, Determining Sound Markings in Structured Nets,
Fundamenta Informaticae, 72, 2006.
[BPM05] M. Laugna, J. Marklund. Business Process Modeling, Simulation, and De-
sign. Prentice Hall, Upper Saddle River, New Jersey, 2005.
[HA00] C.Hagen, G.Alonso, Exception Handling in Workflow Management Systems,
IEEE Trans. of Soft. Eng. vol. 26 No 10, Oct 2000.
[BPS09] W.M.P. van der Aalst, J. Nakatumba, A. Rozinat, and N. Russell. Business
Process Simulation: How to get it right? In J. vom Brocke and M. Rosemann, editors,
International Handbook on Business Process Management, Springer-Verlag, Berlin,
2009.
[WS09] A. Rozinat, M. Wynn, W.M.P. van der Aalst, A.H.M. ter Hofstede, and C.
Fidge., Workflow Simulation for Operational Decision Support., Data and Knowl-
edge Engineering, 68(9):834-850, 2009.