Page 22 -

4 1 Introduction

Fig. 1.1 A Petri net modeling the handling of compensation requests

(and possibly subprocesses). The ordering of these activities is modeled by describ-
ing casual dependencies. Moreover, the process model may also describe temporal
properties, specify the creation and use of data, e.g., to model decisions, and stipu-
late the way that resources interact with the process (e.g., roles, allocation rules, and
priorities).
Figure 1.1 shows a process model expressed in terms of a Petri net [35]. The
model describes the handling of a request for compensation within an airline. Cus-
tomers may request compensation for various reasons, e.g., a delayed or canceled
flight. As Fig. 1.1 shows, the process starts by registering the request. This activity
is modeled by transition register request. Each transition is represented by a square.
Transitions are connected through places that model possible states of the process.
Each place is represented by a circle. In a Petri net a transition is enabled, i.e., the
corresponding activity can occur, if all input places hold a token. Transition regis-
ter request has only one input place (start) and this place initially contains a token
to represent the request for compensation. Hence, the corresponding activity is en-
abled and can occur. This is also referred to as firing. When firing, the transition
consumes one token from each of its input places and produces one token for each
of its output places. Hence, the firing of transition register request results in the
removal of the token from input place start and the production of two tokens: one
for output place c1 and one for output place c2. Tokens are shown as black dots.
The configuration of tokens over places—in this case the state of the request—is
referred to as marking. Figure 1.1 shows the initial marking consisting of one token
in place start. The marking after firing transition register request has two tokens:
one in place c1 and one in place c2. After firing transition register request, three
transitions are enabled. The token in place c2 enables transition check ticket.This
transition models an administrative check to see whether the customer is eligible
to issue a request. For example, while executing check ticket it is verified whether
the customer indeed has a ticket issued by the airline. In parallel, the token in c1
enables both examine thoroughly and examine casually. Firing examine thoroughly
will remove the token from c1, thus disabling examine casually. Similarly, the oc-