=Paper=
{{Paper
|id=None
|storemode=property
|title=Observable Liveness
|pdfUrl=https://ceur-ws.org/Vol-1160/paper9.pdf
|volume=Vol-1160
|dblpUrl=https://dblp.org/rec/conf/apn/DeselK14
}}
==Observable Liveness==
https://ceur-ws.org/Vol-1160/paper9.pdf
Observable Liveness
Jörg Desel1 and Görkem Kılınç1,2
1
Fakultät für Mathematik und Informatik, FernUniversität in Hagen, Germany
2
Universitá degli Studi di Milano-Bicocca, Italy
Abstract. Whereas the traditional liveness property for Petri nets guar-
antees that each transition can always occur again, observable liveness
requires that, from any reachable marking, each observable transition can
be forced to fire by choosing appropriate controllable transitions; hence
it is defined for Petri nets with distinguished observable and control-
lable transitions. We introduce observable liveness and show this new
notion generalizes liveness in the following sense: liveness of a net im-
plies observable liveness, provided the only conflicts that can appear are
between controllable transitions. This assumption refers to applications
where the uncontrollable part models a deterministic machine (or several
deterministic machines), whereas the user of the machine is modeled by
the controllable part and can behave arbitrarily.
1 Introduction
Liveness and boundedness have turned out to be the most prominent behavioral
properties of Petri nets – a Petri net is considered to behave well if it is live and
bounded. This claim is supported by many publications since decades, and in
particular by the nice correspondences between live and bounded behavior of a
Petri net and its structure, see e.g. [4, 11]. Nowadays workflow Petri nets receive
a particular interest, and with them the behavioral soundness property. However,
as shown in [16], soundness of workflow nets is identical to the combination of
liveness and boundedness of the net obtained by addition of a feedback place
(between the final and the initial transition) to a workflow net. This way, these
behavioral properties are also applied to models of processes, that have a start
and an end action.
This paper concentrates on liveness, but looks at yet another scenario: Petri
nets with transitions that can be observable or unobservable (silent transitions),
and can be controllable or not. These nets are inspired by Petri net applications
in control theory [8, 2], but can also be seen as a generalization of Petri nets
with silent transitions. We provide a notion of liveness which is tailored for Petri
nets with observable and controllable transitions, or for the systems modeled by
these nets. Observable liveness of a model of a software system (embedded or
not) with a user interface roughly means liveness from the user’s perspective.
The standard definition of liveness for traditional Petri nets reads as follows:
A transition t is live if, for each reachable marking m, there is a
marking m0 reachable from m that enables t. A net is live if all its
transitions are live.
144 PNSE’14 – Petri Nets and Software Engineering
We consider Petri net models of software systems where only some activities
are observable, and only a subset of these can be controlled by a user (like a vend-
ing machine, which has a user interface and an internal behavior). Our liveness
notion applies to such nets, which also have observable transitions and, among
them, controllable ones. This liveness notion still follows the idea that, no matter
which marking m was reached, an occurrence sequence can be constructed which
includes a given transition t. However, in contrast to the traditional definition,
– we only consider observable transitions t (i.e., if a transition cannot be ob-
served then we do not care about it),
– we assume that instead of constructing the entire sequence, we (i.e., the user)
can only control the net by choosing controllable transitions whenever they
are enabled, whereas the net is always free to fire uncontrollable transitions
arbitrarily. In particular, if a controllable transition is in conflict with an
uncontrollable one, the controllable one might fire but cannot be enforced
by the user.
This paper consists of two main parts with two different aims: In the first
part of the paper we motivate observable liveness notion for observable software
system models. The second part concentrates on the special case where the
uncontrollable part of the considered software system behaves deterministically,
that means conflict situation can only occur between two controllable transitions.
We show that liveness implies observable liveness if no uncontrollable part ever
is in conflict with any other transition. This assumption refers to applications
where the uncontrollable part models a deterministic machine, whereas the user
of the machine is modeled by the controllable part and can behave arbitrarily.
The paper is organized as follows. In Section 2, we introduce our setting
and illustrate a simple example. Section 3 is devoted to basic definitions. In
Section 4 , we introduce the notion of observable liveness. Section 5 discusses
some properties of the new notion and relate it with the traditional liveness.
Section 6 is devoted to the case of deterministic uncontrollable behavior. We
finish the paper with conclusions, related work and further ideas.
2 The Setting
When defining observable liveness, several design decisions had to be made. We
had a particular setting of a modeled system in mind, that motivated our choices.
This section aims at explicating this setting and motivating our design decisions.
The generic software system to be modeled consists of a machine (or several
machines), a user interface to this machine, and perhaps of activities and condi-
tions which do not belong to the machine. The user can observe and control all
activities outside the machine, he can neither control nor observe any activities
inside the machine. Concerning the user interface, there are activities that the
user can only observe but not control, whereas other interface activities might
be both observable and controllable.
J. Desel, G. Kılınç: Observable Liveness 145
One might argue that instead of activities, only local states of machines are
observable, for example a light which can be on or off. Then, instead of observing
this state, in our setting we observe the activities that cause the changes of the
state. In terms of nets, instead of observing a place, we observe the (occurrences
of) transitions in the pre- or post-set of the place.
Controllable activities can be those not connected to the machine or can be
activities of the interface. Whereas a controllable activity outside the machine is
clearly also observable, one might argue that this is not obvious for controllable
interface activities. In fact, if the activity can be caused by pressing a button,
the user cannot be sure that with every use of this button the activity takes
place. An additional prerequisite is that the activity is enabled by the machine,
whereas buttons can always be pressed. So we implicitly assume that the user
sees whether a controllable transition is enabled or not and can thus distinguish
activities from non-activities caused by buttons.
Assume that a user wants to enforce an observable activity a after some
previous run of the system. Then, depending on what he has observed so far,
he should have a strategy to control activities in such a way that eventually
he can observe a. By translating activities to transitions, the same holds for
the Petri net model. The strategy is formalized by a function that maps an
arbitrary sequence of observable transitions to a set of controllable transitions:
if a sequence was observed, then one of these controllable transitions can be
fired. Since the domain of this function is infinite in general, and its co-domain
finite (theoretically exponential in the number of controllable transitions, but
usually linear), different sequences are mapped to the same set. We assume that
the user can effectively compute this function by using, e.g., only a finite history
or an automata based approach. For generality of our approach, we nevertheless
consider a strategy an arbitrary function as above.
There might be states in which controllable activities and uncontrollable ones
are enabled, i.e., both the machinery and the user can do something. In such a
state, we cannot expect that the user is able to do his controllable activity first.
This means that, in case of competition between activities, the user does not
have control if not only controllable activities are involved.
For an observably live activity, we want that the user can enforce the oc-
currence of this activity. Therefore, we provide an appropriate behavioral model
of the net. Clearly, the user can only enforce any reaction from the machine if
the machine obeys some progress assumption: we do not consider runs in which
an uncontrollable transition is enabled, does not occur, and is not in conflict
with any other occurring transition. Progress is only assumed for controllable
transitions if they are persistently chosen by the response function and moreover
concurrent to uncontrollable ones.
Throughout the paper, a controllable transition is illustrated via a black
filled rectangle, an observable transition is illustrated by a bold rectangle, while
unobservable ones are drawn by not bold rectangles. The incoming and outgoing
arcs which are not connected to any place or transition are used when only a
part of a net is shown.
146 PNSE’14 – Petri Nets and Software Engineering
Fig. 1. An observably live net which represents a vending machine.
J. Desel, G. Kılınç: Observable Liveness 147
The example net shown in Fig. 1 models a vending machine with coffee and
tea options. The user can operate the machine by inserting a coin and using
three buttons (insert coin, choose coffee, choose tea and take money back are
controllable transitions). Using these controllers, the user can take coffee, take
tea or take his money back. The transitions coffee comes out, tea comes out and
money comes out are observable, and the user can always force these transitions
to occur by using the controllable ones. In other words, each of the observable
transitions in the net is observably live and so the entire net is observably live.
In case that there is no more coffee or tea, the machine needs a refill operation.
In this case the user has to wait until the refill operation is done. Regarding
the progress assumption, the refill operation will be done since refill coffee and
refill tea transitions will fire eventually, and they are not in conflict with any
transitions which can disable them. Note that the entire net is not live since the
unobservable part includes a transition which can only fire once (init machine).
However, this behavior does not affect our notion of observable liveness since
the observable transitions can still be forced to fire. Considering such a machine,
observable liveness is a useful notion to express the serviceability of a machine
via an interface. We can generalize this for models of all kinds of software systems
with a user interface. In this case, observable liveness expresses the liveness of a
software system from the user’s point of view.
3 Basic Definitions
An (initially marked) place/transition net N consists of a finite and non-empty
set of places P , a finite and non-empty set of transitions T with P \ T = ;, a
set of arcs F ✓ (P ⇥ T ) [ (T ⇥ P ) and an initial marking m0 : P ! N. For a
place or transition x, we denote its pre-set by • x = {y 2 P [ T | (y, x) 2 F }.
Similarly, the post-set of x is denoted by x• = {y 2 P [ T | (x, y) 2 F }.
A marking m is an arbitrary mapping m : P ! N. It enables a transition t
if each place p 2 • t satisfies m(p) > 0. If it enables t then t can fire, which leads
to the successor marking m0 , defined by
8
< m(p) + 1 if p 2 t• , p 2 / •t
0
m (p) = m(p) 1 if p 2 • t, p 2 / t•
:
m(p) otherwise
t
We denote this by m ! m0 .
The set of reachable markings of the net N , R(N ), is the smallest set of
markings that contains the initial marking m0 and satisfies
t
[m 2 R(N ) ^ m ! m0 ] =) m0 2 R(N ).
The place/transition net is called bounded if R(N ) is finite. Equivalently, it is
bounded if and only if there exists a bound b such that each marking m 2 R(N )
satisfies for each place p: m(p) b. It is called 1-bounded if this condition holds
for b = 1.
148 PNSE’14 – Petri Nets and Software Engineering
t t t
If m1 ! 1
m2 ! 2
m3 ! 3
m4 · · · , then t1 t2 t3 t4 . . . is called occurrence
sequence (enabled at marking m1 ). If an occurrence sequence is finite, i.e.
= t1 t2 . . . tn , then we write m1 ! mn+1 .
The place/transition net is live if, for each reachable marking m and each
transition t, there exists a marking m0 reachable from m that enables t. Equiv-
alently, it is live if and only if for each transition t and each finite occurrence
sequence enabled at m0 there exists a transition sequence ⌧ such that ⌧ t is an
occurrence sequence enabled at m0 . Note that in order to append two sequences,
the left hand one is supposed to be finite. In turn, when writing ⌧ we implicitly
express that is finite.
Transitions can be observable or non-observable, and they can be controllable
or non-controllable. We denote by O ✓ T the set of observable transitions and
by C ✓ O the set of controllable ones.
A place/transition net with observable and controllable transitions is called
observable place/transition net N = (P, T, F, m0 , O, C). Given an occurrence
sequence of the place/transition net, its projection to the observable transi-
tions is called observable occurrence sequence. Conversely, a sequence t1 t2 t3 . . .
of observable transitions is an observable occurrence sequence if and only if
there are finite sequences 0 , 1 , 2 , . . . of unobservable transitions such that
0 t1 1 t2 2 t3 . . . is an occurrence sequence.
An infinite occurrence sequence t1 t2 t3 . . . enabled at some marking m is
called weakly unfair w.r.t. some transition t if, for some k 2 N, t1 t2 . . . tk t
is enabled at m and, for each j > k, we have • tj \ • t = ; (after some finite
initial phase, t is persistently enabled and not in structural conflict with any
occurring transition). Notice that this definition is slightly weaker than the usual
definition of weak fairness which only demands that t is persistently enabled. The
occurrence sequence is weakly fair w.r.t. t if it is not weakly unfair w.r.t. t. By this
definition, every finite occurrence sequence is weakly fair w.r.t. to all transitions.
There are many different fairness notions for Petri nets (and previously for
other models). Our notion - often also called progress assumption - was first
mentioned in [12]. It is particularly obvious for partially ordered behavior notions
such as occurrence nets and can now be viewed as a standard notion.
4 Observable Liveness
In order to give the definition of observable liveness, we first stick to observ-
able liveness of a single transition, which apparently has to be observable, and
later define observable liveness of observable place/transition nets as observable
liveness of all observable transitions.
So consider a single observable transition t which might be moreover control-
lable or not. If the net reaches from the initial marking m0 a marking m by the
occurrence of an arbitrary occurrence sequence 0 , an agent wants to enforce
transition t by selecting appropriate controllable, enabled transitions. If this is
always (for each reachable marking m) possible, then we call t observably live.
J. Desel, G. Kılınç: Observable Liveness 149
From the marking m, the net first proceeds arbitrarily and autonomously,
i.e., some occurrence sequence 1 without controllable transitions occur. This
sequence can be
a) finite and lead to a deadlock,
b) finite and lead to a marking that enables controllable and uncontrollable
transitions,
c) finite and lead to a marking that enables only controllable transitions,
d) or infinite.
For the infinite case we demand weakly fair behavior w.r.t. all uncontrollable
transitions, i.e. there is progress in all concurrent parts of the net.
For cases b) and c), the agent fires a controllable transition and then proceeds
as before with a next autonomous sequence 2 , and so on. This will lead to either
an infinite sequence i , or eventually to case a) or case d).
Our liveness notion should express that – in case of observable liveness –
there always is (at least one) controllable transition after any sequence i in
case c). To formalize this, (and to avoid an infinite alternation of 8 and 9) we
introduce a response function ', which delivers a set of possible controllable
transitions as a response of the agent to the sequence observed so far. Notice
that an observed sequence does not determine the reached marking because
unobservable transitions might occur, changing the marking but not effecting
the observed sequence. In turn, different observed sequences might lead to the
same marking.
We call the transition t observably live if, for some such response function,
we eventually observe t in the sequence created this way.
More formally, the definition reads as follows:
Definition 1. Let ' : O⇤ ! 2C be a response function and let m0 0
! m be
an occurrence sequence. We call an occurrence sequence , enabled at marking
m, '-maximal if it is either an infinite composition = 1 t1 2 t2 3 t3 . . . or a
finite composition = 1 t1 2 t2 . . . k tk µ, where k 0, satisfying the following:
a) All i are finite and can be empty, µ is finite or infinite.
b) For each ti we have ti 2 '( 0 1 t1 2 t2 . . . i ), i.e., ti is a response to the
sequence observed so far.
c) No i contains a controllable transition (i 1), and the same holds for µ.
Only for the second variant:
d) µ is weakly fair w.r.t. all non-controllable transitions. µ is moreover weakly
fair w.r.t. all controllable transitions t satisfying t 2
/ '( 0 0 ) for only finitely
many prefixes 0 of .
e) If µ is finite then all transitions enabled after are controllable and do not
belong to '( 0 ) (this includes deadlocks).
Lemma 1. Assume that 0 leads from m0 to a marking m and is a '-maximal
occurrence sequence enabled at m. If = 1 2 and m !1
m1 , then 2 is a
'-maximal occurrence sequence enabled at m1 .
150 PNSE’14 – Petri Nets and Software Engineering
Proof. The claim follows immediately from the definition of '-maximal occur-
rence sequence. t
u
Some comments: All i in Definition 1 are finite and succeeded by a control-
lable transition, chosen by the response function. If we get stuck in a deadlock,
this is the case of a finite µ. We do not expect that after some i only control-
lable transitions are enabled. Therefore, there might be situations where the user
can fire a controllable transition but also the net can proceed autonomously. If
liveness can only be enforced by passivity of the user in this case, the response
function yields the empty set for the observed sequence.
Fig. 2. Some example nets.
Figures 2.a, 2.b, and 2.c illustrate the weak fairness notion employed in our
definition of '-maximal occurrence sequence.
In the net shown in Fig. 2.a., after the controlled occurrence of t1 the system
can choose between t2 and t4 . It can even always prefer t2 , and t4 never occurs.
Only strong fairness would imply that eventually t4 can be observed, but our
chosen notion of weak fairness does not. So t4 is not observably live.
In Fig. 2.b., the net of Fig. 2.a. is extended by a concurrent sequence. Our
weak fairness assumption implies that the left branch proceeds even if the right
stays in an infinite loop. So transition t3 is observably live.
Figure 2.c. illustrates the difference between our weak fairness and the one
usually used in the literature, e.g. [13]. We do not expect that t6 eventually occurs
although it remains enabled at each marking reached after the occurrence of t4 .
J. Desel, G. Kılınç: Observable Liveness 151
However, since t5 and t6 share the input place p5 we do have a conflict here. So
again, t3 is observably live and t6 is not.
Fig. 3. Example nets.
In the net shown in Fig. 3.a, there is a conflict between t3 and t4 . In this
situation, even if the response function ' tells us to fire t4 after t1 , we cannot
be sure that t4 will stay enabled since the unobservable transition t3 might also
fire. Since we cannot force t4 to fire, t5 is not observably live.
Now we define observable liveness as follows:
Definition 2. An observable transition t of an observable place/transition net
is observably live if there is a response function 't : O⇤ ! 2C such that, for
each m0 0
! m, each 't -maximal occurrence sequence enabled at m contains
an occurrence of t. An observable place/transition net is observably live if all its
observable transitions are observably live.
In this definition, “an occurrence of t" can be replaced by “infinitely many
occurrences of t", as in the definition of traditional liveness.
Theorem 1. An observable transition t of an observable place/transition net is
observably live if and only if there is a response function 't : O⇤ ! 2C such
that, for each m0 !0
m, each 't -maximal occurrence sequence enabled at m
contains infinitely many occurrences of t.
Proof. Clearly we only have to prove ), because each occurrence sequence with
infinitely many occurrences of t has at least one t-occurrence.
152 PNSE’14 – Petri Nets and Software Engineering
So assume observable liveness of t, i.e., a response function 't : O⇤ ! 2C
0
such that, for each m0 0
! m0 , each 't -maximal occurrence sequence enabled
at m contains an occurrence of t (notice that we replaced 0 by 00 and m by
0
m0 ).
Let m0 0
! m and let be a 't -maximal occurrence sequence enabled
at m. We have to show that contains infinitely many occurrences of t. By
assumption we know that contains at least one occurrence of t. Let 1 be the
prefix of that ends after the first occurrence of t and let = 1 2 . Then
m0 ! m1 for some marking m1 . This marking m1 enables the 't -maximal
0 1
occurrence sequence 2 by Lemma 1. Again using the assumption, 2 contains
an occurrence of t.
The arbitrary repetition of this argument yields arbitrarily many occurrences
of t in , whence this sequence must have infinitely many t-occurrences. t
u
5 Properties and Relations with Traditional Liveness
In this section, we provide some properties of observable liveness and relations
to traditional liveness.
Lemma 2. For each response function ' and each m0 0
! m, there is a '-
maximal occurrence sequence enabled at m.
Proof. In order to construct a '-maximal occurrence sequence, we proceed it-
eratively. Assume that we constructed a finite sequence 0 , enabled at m, in
0
accordance with a), b) and c) of Def. 1 and let m ! m0 . If m0 enables an
uncontrollable transition t or a controllable one which is in the current response
set '( 0 0 ), then we append t to 0 . If there is more than one such candidate, we
choose the least recently chosen such transition in order to ensure weak fairness.
If this is not possible then all transitions enabled after 0 are controllable and
do not belong to '( 0 0 ), whence then 0 is a '-maximal occurrence sequence
by e) of Def. 1. t
u
Proposition 1. Each observably live transition t is live.
Proof. Since t is an observably live transition there is a response function 't such
that for each m0 0
! m, each 't -maximal occurrence sequence enabled at m
includes t. By Lemma 2 there exists a 't -maximal occurrence sequence. This
implies that, for each reachable marking m, there exists an occurrence sequence
which enables t, and so t is live. t
u
Corollary 1. An observably live net is live if all transitions are observable. t
u
Notice that Cor. 1 does not hold without the assumption that all transitions
are observable. The net shown in Fig. 3.b is not live since t3 can never occur,
but it is observably live.
The converse of Prop. 1 does not hold in general. Figure 2.a, if t4 is assumed
to be connected to t1 , shows a live net which is not observably live. However, if
J. Desel, G. Kılınç: Observable Liveness 153
all transitions are controllable then liveness of t implies its observable liveness,
as shown next:
Proposition 2. If O = C = T then observable liveness of a transition t coin-
cides with its liveness.
Proof. By Prop. 1, we only have to show the implication (.
Assume that t is live. We have to show that there is a response function
't : O⇤ ! 2C such that, for each m0 0
! m, each 't -maximal occurrence
sequence enabled at m contains an occurrence of t. Since t is live, there exists
an occurrence sequence 0 enabled at m such that t is enabled after 0 .
0
t
Let 0 0 t = 0 0 t = t1 t2 t3 . . . tk and m0 0
! . We choose any response
function with 't (t1 t2 . . . ti ) = {ti+1 } for i = 0, 1, . . . , k 1. Since all transitions
are controllable, the unique 't -maximal occurrence sequence consists of only
controllable transitions. The i (for i = 1, 2, 3, . . .) given in Def. 1 are thus
empty sequences, and so there is only one 't -maximal occurrence sequence for
each m. t
u
Corollary 2. If O = C = T , then observable liveness of a net coincides with
liveness of the net. t
u
Proposition 3. Assume that in an observable net there is an infinite and weakly
fair occurrence sequence without controllable transitions. Then each observable
transition which does not appear in infinitely often is not observably live.
Proof. Let m0 0
! m and assume that t is an observably live transition. There
is a response function 't such that each 't -maximal occurrence sequence enabled
at m contains an occurrence of t. So an infinite weakly fair occurrence sequence
without controllable transitions which is enabled at some marking m0 such
0
that m0 0
! m ! m0 ! has to include t to be observably live. Since
the sequence does not include any instance of t, t cannot be observably live.
t
u
Corollary 3. If an observable net without controllable transitions has an infinite
and weakly fair occurrence sequence which does not include all the observable
transitions then the net is not observably live. t
u
6 Deterministic Uncontrollable Behavior
As seen before, a live net is not necessarily observably live. The main reason
is that, for proving liveness, we can always choose an appropriate occurrence
sequence enabling some transition t whereas for observable liveness this choice
is only possible for controllable transitions (which are not in conflict with unob-
servable ones) and the net behaves arbitrarily elsewhere.
In this section, we show that the situation is different if the only choices
to be made are among controllable transitions. This is not an unrealistic set-
ting; the automated part of a system often behaves deterministically (but still
concurrently), whereas the user model might allow for alternatives.
154 PNSE’14 – Petri Nets and Software Engineering
Formally, deterministic behavior is given in terms of the conflict-free property,
to be defined next. Intuitively, a transition is conflict-free if it is never in conflict
with any other transition; if both are enabled then they are enabled concurrently.
Since “never" refers to reachable markings, the definition applies to a net with
an initial marking and its state space and not only to its structure. However,
each two transitions that are ever in conflict necessarily share an input place
which is thus forward branching. With concurrent behavior we mean that two
transitions do not compete for tokens. If a place carries more than one token,
one could argue that two transitions in its post-set still can occur concurrently
(see [17]). We take the stricter view that every two enabled transitions with a
common input place (which can carry one or more tokens) are considered in
conflict and not concurrent.
Definition 3. A Petri net is conflict-free w.r.t. a transition u if, for each reach-
able marking m enabling u, every other transition v enabled at m is concurrent
to u, i.e., • u \ • v = ;.
Figure 3.c shows a net fragment which is conflict-free w.r.t. all its unob-
servable transitions. Notice that there is concurrency between these transitions.
Notice also that forward branching places are possible, provided every reachable
marking enables at most one output transition of a branching place. The follow-
ing lemma will be used frequently in the sequel. It follows immediately from the
occurrence rule.
Lemma 3. Assume two transitions u and v of a net, both enabled at some
marking m, such that • u \ • v = ;. Then m enables u v as well as v u, and both
sequences lead to the same marking. t
u
A well-known result for conflict-free nets [10] is given by the following lemma.
We provide a proof for the sake of self-containment, and since our lemma refers
to a single conflict-free transition only.
Lemma 4. If a Petri net is conflict-free w.r.t. a transition u, and some reach-
able marking m enables u as well as a sequence u where u does not appear in
, then m also enables the sequence u , and the occurrences of u and of u
lead to the same marking.
Proof. By induction on the length of .
Base: If is the empty sequence then nothing has to be shown.
Step: Assume = v 0 . We have u 6= v because u does not appear in . By
conflict-freeness w.r.t. u and since m enables both u and v, these transitions are
concurrent. Therefore, and by Lemma 3, m also enables the sequences v u and
v
v 0 u. Let m ! m0 .
The induction hypothesis can be applied to the marking m0 , enabling u and
0
u, yielding the sequence u 0 enabled at m0 . So v u 0 is enabled at m. Again
since u and v are concurrent and by Lemma 3, m also enables u v 0 , which is
identical with u .
J. Desel, G. Kılınç: Observable Liveness 155
Since each transition occurs in u and in u the same number of times,
and by the occurrence rule, the occurrences of these sequences lead to the same
marking. t
u
Lemma 5. If a Petri net is conflict-free w.r.t. a transition u, and some reach-
able marking m enables u as well as a sequence where u does not appear in ,
then m also enables the sequence u.
Proof. By induction on the length of .
Base: If is the empty sequence then nothing has to be shown.
Step: Assume = v 0 . We have u 6= v because u does not appear in . By
conflict-freeness w.r.t. u and since m enables both u and v, these transitions are
concurrent. Therefore, and by Lemma 3, m also enables the sequence v u. Let
v
m ! m0 .
The induction hypothesis can be applied to the marking m0 , enabling u and
0
, yielding the sequence 0 u enabled at m0 . So v 0 u is enabled at m. We have
v 0 = , which finishes the proof. t
u
The following theorem constitutes the main result of this paper. It applies
only to nets where the only possible conflicts occur between controllable tran-
sitions, i.e., to nets which are conflict-free w.r.t. all uncontrollable transitions.
This rules out conflicts between two uncontrollable transitions as well as conflicts
between controllable and uncontrollable transitions.
As a preparation, we need a couple of definitions and lemmas.
Definition 4. An occurrence sequence enabled at a marking m is called min-
imal towards t, where t is a transition, if ends with t, contains no other
occurrence of t, and no transition in can be postponed, i.e., = 0 t, t does
not occur in 0 , and cannot be divided as = µ0 u µ00 for some transition u,
u 6= t, such that µ0 µ00 is enabled at m, too.
A transition u can only occur if its input places carry tokens, and another tran-
sition v might have to occur before because it produces the token consumed by
u. We then call the occurrence of v a causal predecessor of the occurrence of u. A
minimal occurrence sequence towards a transition t contains one occurrence of t,
its causal predecessors, the predecessors of these predecessors etc., and nothing
else. In partially ordered runs, where causal dependence between transition oc-
currences is explicitly modeled by means of a partial order, this corresponds to
a run containing the occurrence of t and all transition occurrences that precede
t.
Definition 5. Given a sequence , any deletion (i.e, replacement by the empty
sequence) of elements in yields a subsequence of . Its complementary se-
quence is the sequence obtained from by deleting all elements that appear in
the subsequence.
This definition captures the case = 0 00 where 0 is a subsequence and
00
is its complementary sequence (and vice versa), but is more general. For
example, if = t1 , t2 , . . . , t2n , the sequence t1 , t3 , . . . , t2n 1 is a subsequence,
and t2 , t4 , . . . t2n its complementary sequence.
156 PNSE’14 – Petri Nets and Software Engineering
Lemma 6. Assume a conflict-free net with a reachable marking m, a transition
t and an occurrence sequence enabled at m that contains an occurrence of t.
Then there exists a subsequence 0 of , enabled at m, which is minimal towards
t. Moreover, if 00 is the complementary subsequence, m enables 0 00 .
Proof. Define µ as the prefix of which ends with the first occurrence of t, and
let µ be the rest of . Clearly, µ is finite.
Assume that µ can be divided as µ = µ0 u µ00 such that µ0 µ00 is enabled at
m and u does not occur in µ00 . By Lemma 5, we can shift u behind µ00 and thus
obtain the sequence µ0 µ00 u. Still t occurs only once, being the last transition in
µ00 .
If u1 is the rightmost transition (transition occurrence, respectively) in µ for
which such a division is possible, we obtain from µ µ the sequence µ01 µ001 u1 µ.
Let µ2 = µ01 µ001 . Now let u2 be the rightmost transition with the same property
for the sequence µ2 and let µ2 = µ02 u2 µ002 . The same argument as above yields
the sequence µ02 µ002 u2 u1 µ. Exhaustive repetition of this procedure yields smaller
and smaller sequences µi to be considered and eventually the sequence
µ0k µ00k uk uk i . . . u1 µ
such that no further transition to be postponed can be found in µ0k µ00k . So this
sequence is minimal towards t. By construction, it is a subsequence of , and
uk uk i . . . u1 µ is the complementary subsequence. t
u
Starting with the next lemma, we additionally require 1-boundedness, i.e.,
we assume that no reachable marking assigns more than one token to a place.
Lemma 7. Consider a 1-bounded and conflict-free Petri net with an arbitrary
transition t. All initially enabled occurrence sequences which are minimal towards
t lead to the same marking.
Proof. Consider two occurrence sequences µ1 and µ2 , both enabled at the initial
marking, and both minimal towards t. We proceed by induction on the length
of µ1 .
Base: The sequence µ1 has only one element if and only if µ1 = t. So then t
is initially enabled, and hence µ1 = µ2 = t.
Step: Assume that t is not initially enabled. We claim that there is an initially
enabled transition u which appears in µ1 as well as in µ2 , i.e., µ1 = µ01 u µ001 and
µ2 = µ02 u µ002 . When this claim is proven, we know by conflict-freeness that
there are also initially enabled occurrence sequences u µ01 µ001 and u µ02 µ002 . By the
induction hypothesis applied to the (new initial) marking obtained by firing u
and to the sequences µ01 µ001 and µ02 µ002 , both sequences lead to the same marking,
and we are finished.
So it remains to prove the claim, that some initially enabled transition occurs
in µ1 and in µ2 . We proceed indirectly and assume the contrary.
We again divide µ2 as µ02 µ002 , now such that no transition of µ02 occurs in
µ1 and the first transition in µ002 , say v, occurs in µ1 . By assumption, v is not
J. Desel, G. Kılınç: Observable Liveness 157
initially enabled. The sequence µ002 is not empty because both µ1 and µ2 contain
t. We divide µ1 as µ01 µ001 such that µ001 begins with the first occurrence of v in µ1 .
Since v is not enabled initially, some place s 2 • v is initially unmarked.
Since v is enabled after µ01 and after µ02 , s carries a token after the occurrence
of µ01 and after the occurrence of µ02 . By conflict-freeness and since the sets of
occurring transitions in µ01 and µ02 are disjoint, we can also fire both, i.e. µ01 µ02 ,
from the initial marking. This yields a marking with two tokens on the place s,
contradicting 1-boundedness. t
u
The proof of the above lemma also shows that all minimal sequences towards
t have the same length, whence these sequences are exactly the sequences with
minimal length containing an occurrence of t.
Now we are ready for the main result: liveness of a 1-bounded net implies
observable liveness, provided the only conflict that can appear are between con-
trollable transitions. Although this result might seem obvious at first sight, its
proof is surprisingly involved. The core argument of the proof is that, in a live
Petri net, for each transition t, every reachable marking m enables an occurrence
sequence m that includes an occurrence of t. If t is observable, then observable
liveness requires that we can force t to occur by only providing a suitable re-
sponse function 't which controls the behavior whenever there is a conflict. So
an obvious idea is to define 't in such a way that always the next transition
in m is responded, if this transition is controllable. However, 't depends not
on markings, but on observed sequences. That means, instead of t the user only
knows the sequence of observable transitions of the initially enabled occurrence
sequence 0 that leads to m. For this observed sequence, there might exist many
sequences including unobservable transitions, and hence many different reached
markings m, and so also many different occurrence sequences m . Instead of the
unknown occurrence sequence 0 we consider the set of all occurrence sequences
µ0 satisfying µ0 = 0 . Among these sequences we concentrate on the minimal
ones. We will show that, if the net is 1-bounded, all these minimal occurrence
sequences lead to the same marking which we call m 0 . We will moreover show
that m, the marking reached by the occurrence of 0 is reachable from m 0 .
However, these results only hold for conflict-free nets, and our considered net is
not necessarily conflict-free. Since until now we only consider the behavior given
by the observed transitions of 0 , since all controllable transitions are observable
and since conflicts only appear among controllable transitions, we can transform
the considered net into a conflict-free one, without spoiling the relevant behavior.
By liveness (of the original net), m 0 enables an occurrence sequence contain-
ing t. First, we look at the first observable transition in . Since there are no
conflicts, every occurrence sequence starting at m 0 possessing a weak fairness
assumption eventually has to enable u. If u is controllable, it might be in conflict
with some other transition. In this case we set 't ( 0 = {u}) so that, if u is con-
trollable or not, also u eventually occurs. Fortunately, the distance between this
marking and a marking enabling t is smaller than the distance between m and a
marking enabling t, where distance is defined in terms of the number of needed
observable transitions to reach one marking from the other. So we can repeat the
158 PNSE’14 – Petri Nets and Software Engineering
above considerations, this way defining 't on the fly, until we eventually force t
to occur.
Theorem 2. If a 1-bounded observable Petri net, which is conflict-free w.r.t. all
uncontrollable transitions, is live, then it is observably live.
Proof. Consider a 1-bounded live observable Petri net which is conflict-free w.r.t.
all uncontrollable transitions. We have to prove observable liveness, i.e., observ-
able liveness of each observable transition t. So let t be an observable transition.
To show observable liveness of t, we have to provide a response function 't such
that, for each m0 0
! m, each 't -maximal occurrence sequence enabled at
m eventually contains t.
The considered net is only partially conflict-free, because there might be con-
flicts between controllable transitions. To be able to apply the previous lemmas,
we make the net conflict-free for a given initially enabled sequence µ0 :
For each observable transition v we add a fresh place sv , and an arc from
sv to v. Then v can only occur when sv is marked. Now consider the sequence
µ0 = v1 v2 . . . vk . For each transition vi in this sequence except the last (vk ) we
add an arc from vi to svi+1 . The place sv1 gets an initial token, the other new
places remain unmarked initially.
By construction, every reachable marking of this extended net marks at most
one of the new places. Since each observable transition has such a place in its pre-
set, always at most one observable transition is enabled. Since conflicts are only
possible between controllable transitions and since each controllable transition is
observable, thus no conflict can appear. Therefore, this extended net is conflict-
free. By construction, the new initial marking enables µ0 in the extended net.
The following claim also refers to an arbitrary initially enabled occurrence
sequence µ0 and to the net extended with the places as mentioned above. It
generalizes Lemma 7:
Claim: All minimal occurrence sequences µ enabled at m0 which satisfy µ =
µ0 lead to the same marking.
Proof of Claim: by induction on the length of µ0 .
Base: If µ0 is empty then the only minimal sequence µ satisfying µ = µ0 is
the empty sequence.
Step: Let µ1 , µ2 be minimal occurrence sequences enabled at m0 which satisfy
µ1 = µ2 = 0 .
Let µ1 = u1 u2 . . . uk and let ui be the first observable transition in µ1 .
Similarly, let µ2 = v1 v2 . . . vl . Then the first observable transition vj in µ2
satisfies ui = vj .
We apply Lemma 6 to both sequences and thus obtain minimal subsequences
towards ui (vj , respectively). By Lemma 7, both subsequences lead to the same
marking. The induction hypothesis applies to the two complementary sequences.
This ends the proof of the claim.
The unique (for a given µ0 ) marking reached by a minimal sequence µ sat-
isfying µ = µ0 will be called mµ0 in the sequel. Abusing notation, we call the
same marking of the original net also mµ0 , ignoring the additional places.
J. Desel, G. Kılınç: Observable Liveness 159
In the following, it will be useful to assume an arbitrary fixed total order
on the set of observable transitions, i.e., if u and v are distinct observable
transitions then either u v or v u.
By liveness of the original net, for each initially enabled occurrence sequence
µ0 there exists (at least one) occurrence sequence µ00 ending with t which is
enabled by mµ0 (in the original net). We assume that µ00 has a minimal number
of observable transitions among all sequences with the above property, i.e., µ00
has minimal length. Among these minimal sequences we assume moreover that
the first observable transition in µ00 is minimal w.r.t. .
Now we define 't as follows: For each initially enabled occurrence sequence
µ, we set 't (µ) = {u} if µ0 begins with u and u is controllable, and 't (µ) = ; if
µ0 begins with u and u is not controllable. Notice that µ0 contains t as its last
transition and is hence not empty.
We now come back to the core of this proof and consider an arbitrary initially
enabled occurrence sequence 0 which leads to a marking m. We have to show
that each 't -maximal occurrence sequence enabled at m eventually contains t.
We consider a conflict-free variant of the net as before, but instead of consid-
ering only the sequence 0 we add places according to the sequence 0 't ( 0 ),
i.e., we allow to fire the observable transition 't ( 0 ) after 0 .
We proceed by induction on the number of observable transitions in 00 (which
is defined above as an occurrence sequence ending with t enabled at m 0 with a
minimal number of observable transitions).
Base: Assume that 00 = t. Then there is an occurrence sequence 00 , enabled
at m 0 which eventually contains t (and no other observable transition). Since
m is reachable from m 0 by Lemma 6, for each 't -maximal occurrence sequence
enabled at m there is a suitable prefix yielding a 't -maximal occurrence sequence
from m 0 . By conflict-freeness of the extended net and by weak fairness, each
't -maximal occurrence sequence enabled at m 0 eventually contains t. Hence
this holds in particular for those passing through m.
Step: Assume that 00 = u1 u2 . . . uk t, k 1. Arguing as in the Base case,
there is an occurrence sequence 00 , enabled at m 0 which eventually contains u1
(and no other observable transition). Since m is reachable from m 0 by Lemma
6, for each 't -maximal occurrence sequence enabled at m there is a suitable
prefix yielding a 't -maximal occurrence sequence from m 0 . By conflict-freeness
of the extended net and by weak fairness, each 't -maximal occurrence sequence
enabled at m 0 eventually contains u1 . Hence this holds in particular for those
passing m. So each 't -maximal occurrence sequence enabled at m can be
divided as 1 u1 2 where 2 is again 't -maximal, and 2 is shorter than . By
the induction hypothesis, 2 contains t, and therefore so does . t
u
In Fig. 4, we see one net with a conflict and a conflict-free net. The net
shown in Fig. 4.a includes a conflict between a controllable transition and an
uncontrollable transition (which is also unobservable). Although the net is live,
since we cannot force t1 to fire, both t1 and t3 are not observably live and so the
net is not observably live. When the conflict in Fig. 4.a is resolved, we get the
net shown in Fig. 4.b which is both live and observably live.
160 PNSE’14 – Petri Nets and Software Engineering
Fig. 4. a: a net with a conflict, b: a conflict-free net, c: a net which is conflict-free
w.r.t. its uncontrollable transitions.
The net shown in Fig. 4.c is conflict-free w.r.t. all its uncontrollable tran-
sitions. Notice that there is a conflict between two controllable transitions t4
and t5 . We can choose the related controllable transition in order to observe the
occurrence of any observable transitions. The only choice is ours to make, the
uncontrollable part of the machine behaves deterministically. This net is both
live and observably live.
7 Conclusion and Related Work
Petri nets are widely used in software engineering for modeling and verifying
software systems [3]. In this work, we provide a novel liveness notion which
expresses the serviceability of a software system via an interface.
We considered a variant of Petri nets with observable transitions, where an
observable transition can also be controllable. For further information about
controllability and observability in Petri nets and using Petri nets in control
theory, see [2, 15].
In analogy to the usual definition of liveness of a Petri net, we provided
a notion for observable liveness, which roughly means that a user can always
enforce the occurrence of any observable transition, only by stimulating the net
by choosing appropriate enabled controllable transition. Therefore it is necessary
to assume that also the uncontrollable part of a net proceeds, i.e., we assume
J. Desel, G. Kılınç: Observable Liveness 161
that the net behaves weakly fair. A similar notion, T -liveness, yet for different
motivations, is represented in [9]. One of the main differences is that only the
fully controllable and observable nets are considered.
In general, liveness does not imply observable liveness and neither the op-
posite direction holds. This paper proves that for 1-bounded Petri nets with
transitions that can be observable or additionally controllable, liveness implies
observable liveness, where the latter means that control can force every transi-
tion to fire eventually from an arbitrary reachable marking – provided the net
model behaves deterministically in its uncontrollable part. This control can only
select enabled controllable transitions and is based only on the sequence of tran-
sitions observed so far. This way the result generalizes the obvious observation,
that in a fully deterministic net a transition is live if and only if it eventually
fires.
A future consideration refers to possible generalizations of our result. It
clearly still holds when there is some limited nondeterminism in the uncon-
trolled part. For example, if two alternative uncontrollable transitions cause the
same marking transformation, the result is not spoiled. More generally, we aim
at defining an equivalence notion on nets, based on the respective observed be-
havior, which preserves observable liveness. Reduction rules, as defined e.g. in
[1], [6] and [4] but also in many other papers, could be applied to the uncon-
trollable part leading to simpler but equivalent nets. However, there are obvious
additional rules. For example, a rule that deletes a dead transition is sound w.r.t.
the equivalence because dead uncontrollable transitions do not contribute to the
observable liveness or non-liveness of the considered net.
As a future work, we plan to consider an automata approach for the im-
plementation of the response function. The domain of the response function is
defined infinite. In order to decide which controllable transitions can be fired
next, an arbitrary history of observed transitions has to be considered. Often, a
finite amount of the history is enough for this decision. If this is the case, an au-
tomata based approach can be used for the realization of the response function:
the response then only depends on a state (of finitely many) of this automaton.
Concerning behavior, each run has an alternation between free choices of the
machine (where in analysis all possibilities must be considered) and particular
choices of the user. Therefore, describing the behavior with AND/OR-trees seems
promising, maybe in combination with unfolding approaches. The partial order
view would have obvious advantages to capture the progress assumption (that
we called weak fairness) in a natural way [5, 14].
A final remark concerns the relation to Temporal Logics. Since liveness and all
reachability questions in traditional Petri nets use existential quantification on
paths (of the reachability graph), and therefore require Branching Time concepts,
our approach explicates reasons for desired activities, i.e., transition occurrences.
More precisely, as in the discussion of liveness in this paper, we distinguish
uncontrollable alternatives and controllable choices, to be able to express that a
certain activity (of a user) leads to the eventual occurrence of an event, no matter
how the uncontrollable activities behave (but assuming they do not refuse work
162 PNSE’14 – Petri Nets and Software Engineering
at all). This is clearly a Linear Time property. So, very roughly speaking, we
translate Branching Time properties to Linear Time properties, and at the same
time add details about controllability and observability to the system model.
Future work aims at these transformations not only in the context of liveness
properties but for arbitrary properties expressed by logical formulae. A related
work has been done by Haddad et al. in [7].
Acknowledgements
The authors thank to Lucia Pomello and Luca Bernardinello for their valuable
comments. This work was partially supported by MIUR and by MIUR - PRIN
2010/2011 grant ‘Automi e Linguaggi Formali: Aspetti Matematici e Applica-
tivi’, code H41J12000190001.
References
1. Gérard Berthelot. Transformations and decompositions of nets. In Wilfried Brauer,
Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advances in Petri Nets, volume
254 of Lecture Notes in Computer Science, pages 359–376. Springer, 1986.
2. Christos G. Cassandras and Stephane Lafortune. Introduction to Discrete Event
Systems. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006.
3. Giovanni Denaro and Mauro Pezzè. Petri nets and software engineering. In Jörg
Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency
and Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 439–466.
Springer Berlin Heidelberg, 2004.
4. J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge tracts in theoretical
computer science. Cambridge University Press, 1995.
5. Jörg Desel, Hans-Michael Hanisch, Gabriel Juhás, Robert Lorenz, and Christian
Neumair. A guide to modelling and control with modules of signal nets. In Hartmut
Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard
Schnieder, and Engelbert Westkämper, editors, SoftSpez Final Report, volume 3147
of Lecture Notes in Computer Science, pages 270–300. Springer, 2004.
6. Serge Haddad. A reduction theory for coloured nets. In Grzegorz Rozenberg,
editor, European Workshop on Applications and Theory in Petri Nets, volume 424
of Lecture Notes in Computer Science, pages 209–235. Springer, 1988.
7. Serge Haddad, Rolf Hennicker, and MikaelH. Møller. Specification of asynchronous
component systems with modal i/o-petri nets. In Martín Abadi and Alberto
Lluch Lafuente, editors, Trustworthy Global Computing, Lecture Notes in Com-
puter Science, pages 219–234. Springer International Publishing, 2014.
8. Lawrence E. Holloway, Bruce H. Krogh, and Alessandro Giua. A survey of petri net
methods for controlled discrete event systems. Discrete Event Dynamic Systems,
7(2):151–190, 1997.
9. Marian V. Iordache and Panos J. Antsaklis. Design of t-liveness enforcing super-
visors in petri nets. IEEE Trans. Automat. Contr., 48(11):1962–1974, 2003.
10. L. H. Landweber and E. L. Robertson. Properties of conflict-free and persistent
petri nets. J. ACM, 25(3):352–364, July 1978.
11. T. Murata. Petri nets: Properties, analysis and applications. In Proceedings of the
IEEE, volume 77, pages 541–580, April 1989.
J. Desel, G. Kılınç: Observable Liveness 163
12. Wolfgang Reisig. Partial order semantics versus interleaving semantics for csp-like
languages and its impact on fairness. In Proceedings of the 11th Colloquium on
Automata, Languages and Programming, pages 403–413, London, UK, UK, 1984.
Springer-Verlag.
13. Wolfgang Reisig. Elements of distributed algorithms: modeling and analysis with
Petri nets. Springer, 1998.
14. Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Meth-
ods, Case Studies. Springer, 2013.
15. Manuel Silva. Half a century after carl adam petri’s ph.d. thesis: A perspective on
the field. Annual Reviews in Control, 37(2):191 – 219, 2013.
16. Wil M. P. van der Aalst. The application of petri nets to workflow management.
Journal of Circuits, Systems, and Computers, 8(1):21–66, 1998.
17. Rob J. van Glabbeek, Ursula Goltz, and Jens-Wolfhard Schicke. On causal seman-
tics of petri nets. In Joost-Pieter Katoen and Barbara König, editors, CONCUR,
volume 6901 of Lecture Notes in Computer Science, pages 43–59. Springer, 2011.