Page 120 -

3 Advanced Synchronization 107
not easy to model in Petri nets. For OR-join analysis, cancelation plays an important
role and it is not possible to abstract from cancelation regions. Hence, we need a
formalism that can support the notion of cancelation regions. Reset nets are Petri
nets extended with reset arcs that remove tokens from reset places when a transition
fires (see Chap. 2) and reset arcs can capture the behavior of the cancelation regions
supported by YAWL. Hence, we define the formal semantics of the OR-join using
reset nets.
The complexity introduced by a reset arc (when compared with classical Petri
nets) is threefold: (1) as the transition removes all tokens and not just one when it
fires, place invariants do not hold for such nets, (2) the reset action can be ineffective
if a place does not contain any tokens at the exact time when the transition fires
and the reset action is carried out, and (3) a reset arc can affect any place in the
entire net (i.e., its effect is global), unlike normal arcs of a transition which can
only influence their input and output places (i.e., their effect is local). As a result,
the notion of reachability is undecidable for reset nets with more than two reset
arcs. Hence, to define the formal semantics of an OR-join, we use the notions of
backwards firing and coverability in reset nets. Coverability is a weaker notion than
reachability; a marking is coverable from another marking if there is a sequence of
tasks that can fire from the first marking to arrive at a marking equal to or bigger
than the second marking (for a formal definition see Chap.2). Normally, a transition
fires at a marking to reach a new marking and we can consider the state as moving
forward. Backward firing a transition, on the other hand, allows us to start from
a desired marking (e.g., a marking where an OR-join is enabled) and transitions
can be fired backwards to see if an initial marking is coverable. A new (backwards
coverable) marking is created, which puts one token into all input places of the
transition which are not reset places, removes one token from all output places of
the transition which are not reset places, and puts one token in all reset places of the
transition. Backwards firing a transition in a reset net is only possible at a marking
if there are no tokens in the reset places of that transition. The backwards firing
rule returns a coverable marking and not necessarily a reachable marking as it is
impossible to know how many tokens originally existed in the reset places.
Using this notion of coverability in reset nets, the semantics of an OR-join can
be defined as follows. An OR-join in a YAWL net is enabled at a given marking M
(where one or more input conditions of the OR-join have tokens) if and only if there
is no marking in the future states of the corresponding reset net that covers M.
To perform an OR-join evaluation using reset net semantics, it is necessary to
first transform a YAWL net into a corresponding reset net for the OR-join of interest.
Formal mappings have been proposed to carry out this transformation. Figure 3.4
summarizes how the various YAWL elements are mapped to reset net places and
transitions. In general, a YAWL task is mapped to two transitions (one that cor-
responds to the start of the task (ts) and one that corresponds to the end of the
task (te) as well as a place in between (pt)). Various splits and joins in YAWL
are also mapped to corresponding places and transitions in reset nets. Conditions
and tasks within a cancelation region of a task are mapped to reset places for the
corresponding transitions, represented by double-headed arcs in the diagram.