=Paper=
{{Paper
|id=Vol-2138/paper1
|storemode=property
|title=Checking Weak Observable Liveness on Unfoldings Through Asynchronous Games
|pdfUrl=https://ceur-ws.org/Vol-2138/paper1.pdf
|volume=Vol-2138
|authors=Luca Bernardinello,Lucia Pomello,Adrián Puerto Aubel,Alessandro Villa
|dblpUrl=https://dblp.org/rec/conf/apn/BernardinelloPA18
}}
==Checking Weak Observable Liveness on Unfoldings Through Asynchronous Games==
https://ceur-ws.org/Vol-2138/paper1.pdf
Checking Weak Observable Liveness
on Unfoldings Through Asynchronous Games
Luca Bernardinello, Lucia Pomello,
Adrián Puerto Aubel, and Alessandro Villa
Dipartimento di Informatica, Sistemistica e Comunicazione
Università degli Studi di Milano-Bicocca
viale Sarca 336-U14, I-20126, Milano, Italy
Abstract. We define an asynchronous two-player game, played on the
unfolding of a Petri net. The set of transitions of the net is partitioned
among the two players, and a play is a run of the unfolding. The role of
the two players is different: we assume that one of them (the User ) has
the right to block transitions under its control, while the other player (the
System) must ensure progress of its transitions. We then define a notion
of strategy for the User. In this framework, one can set different aims
for the two players. Here, we consider the problem of weak observable
liveness, in which the User tries to enforce liveness of a given transition.
We show that a transition is weakly observably live if and only if the
User has a winning strategy in the game.
Keywords: Petri nets, asynchronous games, weak observable liveness,
model-checking
1 Introduction
The problem of weak observable liveness can be stated as follows. A Petri net
models a User interacting with a System. Each transition in the net represents an
action, performed either by the User (controllable transitions) or by the System
(uncontrollable transitions). Actions can be performed concurrently, according to
the structure of the net. The interaction between the two entities is mediated by
the structure of the net, which enforces specific relations between the transitions.
In the general setting, we assume that only some of the uncontrollable transitions
are observed by the User.
One of the transitions is chosen as the target. The User, by firing or blocking
controllable transitions, tries to ensure that in any run of the net, the target
fires infinitely often. To this aim, the User applies a response functions, which,
on the basis of which transitions have been observed to fire so far, chooses which
controllable transition to fire.
In a previous paper ([1]) a restricted version of the problem was translated
into an infinite game on a finite graph (where the finite graph is essentially de-
rived from the marking graph). In that approach the concurrency in the original
model was reduced to its interleaving semantics; this proved to be the source of
16 PNSE’18 – Petri Nets and Software Engineering
several difficulties. Hence, we conceived the idea of a game where moves are not
strictly sequential. Since here we aim at translating the original notion of weak
observable liveness as faithfully as possible, a natural choice was that of working
on the unfolding of the given Petri net. We have then defined a game, played on
the unfolding of a controlled elementary net system, that is an elementary net
system whose transitions are partitioned into ‘controllable’ and ‘uncontrollable’.
A play in this game is a run within the unfolding, together with a sequence of
B-cuts, which can be seen as ‘snapshots’ of the system taken during the play.
Between a snapshot and the next, several transitions can fire, either concurrently
or not.
We expect this game to have a more general interest than just its application
to weak observable livess. In this paper, we discuss this application, and impose
a rather strict limitation, which we plan to remove in the future: we assume that
all transitions are observable. In this framework, we define a strategy for the
User as a map from the set of B-cuts of the unfolding to the set of controllable
events, and prove that, for the family of response functions which always choose
at most one controllable transition, the target is weakly observably live if, and
only if, the User has a winning strategy in the associated game.
Several approaches to the general idea of concurrent and asynchronous games
have been proposed, mainly in the fields of semantics and of verification. In the
introduction of [7], Melliès and Mimram survey the history of the idea, with a
special focus on the application to semantics.
An approach to verification is described in [6]. More recently, Winskel de-
scribed his attempt to build a general theory of distributed games ([10]), using
event structures, which have a strong relation to occurrence nets.
More specifically based on Petri nets and unfolding is the approach proposed
in a series of recent papers (see, for example, [5, 4]). The players in this game
are the tokens of a Petri net. The past of a token at some point in the unfolding
of the net represents the knowledge upon which a token-player can build its
strategy.
The paper is organized as follows. Section 2 introduces preliminary defini-
tions. In particular, after the basic definitions on elementary net systems and
unfoldings given in Section 2.1, Section 2.2 recalls the definitions and facts which
are related to the notions of weak observable liveness and of response functions;
Section 2.3 collects some new facts about response functions, which will be used
in the rest of the paper. Section 3 contains the definition of the game, and
Section 4 the translation of the problem of weak observable liveness into an
equivalent one on the unfolding of the net system, with the appropriate notion
of strategy. Section 5 closes the paper with some remarks.
2 Preliminary Definitions
In this section we collect basic definitions and facts about Petri nets and weak
observable liveness.
Bernardinello et.al.: Checking Weak Observable Liveness with Games 17
2.1 Elementary Net Systems and Unfoldings
The following definitions are adapted from [8] and [9].
An elementary net is a triple N = (P, T, F ), where P and T are disjoint sets.
The elements of P are called places, the elements of T are called transitions.
F is called flow relation, with F ⊆ (P × T ) ∪ (T × P ). By F ∗ we denote the
reflexive and transitive closure of F . Let x ∈ P ∪ T be an element of the net, the
pre-set of x is the set • x = {y ∈ P ∪ T | (y, x) ∈ F }, the post-set of x is the set
x• = {y ∈ P ∪ T | (x, y) ∈ F }. We assume that any transition has non-empty
pre-set and post-set: ∀t ∈ T , • t 6= ∅ and t• 6= ∅. A net is infinite if P ∪ T is
infinite, finite otherwise.
A subnet of N = (P, T, F ) is an elementary net N 0 = (P 0 , T 0 , F 0 ) such that
P ⊆ P , T 0 , ⊆ T , and F 0 is F restricted to the elements in N 0 .
0
An elementary net system is a quadruple Σ = (P, T, F, m0 ) consisting of a
finite elementary net N = (P, T, F ) and an initial marking m0 ⊆ P . A marking
is a subset of P and it represents a global state.
A transition t is enabled at a marking m, denoted m[ti, if • t ⊆ m ∧ t• ∩ m = ∅.
A transition t, enabled at m, can fire producing a new marking m0 = t• ∪ m \ • t,
denoted m[tim0 .
Two transitions, t1 and t2 , are independent if (• t1 ∪ t•1 ) and (• t2 ∪ t•2 ) are
disjoint. A step at a marking m is a set of pairwise independent transitions, all
enabled at m.
A sequence of transitions σ = t1 t2 t3 . . . - finite or not - is enabled at m if
m[t1 im1 [t2 im2 [t3 i . . . . If σ is enabled at a marking then it is called transition
sequence. A transition sequence is called initial transition sequence, or simply
initial sequence, if enabled in the initial marking. The set of initial sequences of
Σ is denoted by seq(Σ). Let i ∈ N : i < |σ|; then t1 t2 . . . ti is called prefix of σ,
denoted by σi . If σ is finite and enabled at m then we write m[σimn and say
that mn is reachable from m. The set of reachable markings of an elementary
net system is the set of markings reachable from the initial marking m0 , denoted
[m0 i.
Let σ ∈ T ∗ be a transition sequence; m(σ) denotes the marking reached by
the system after the occurrence of σ. Taking to denote the empty sequence, we
set m() = m0 .
A marking m is a contact for a transition t if • t ⊆ m and there is p ∈ t• ∩ m.
A net system is contact-free if no reachable marking is a contact.
A transition t is 1-live if there is a reachable marking in which t is enabled.
An elementary net system is 1-live if all its transitions are 1-live.
In this paper, we tacitly assume that the elementary net systems referred to
are contact-free and 1-live.
Let N = (P, T, F ) be a net. Two elements x, y ∈ P ∪ T are said to be in conflict,
denoted x#y, iff there exist t1 , t2 ∈ T : t1 6= t2 , t1 F ∗ x, t2 F ∗ y ∧ ∃p ∈ • t1 ∩ • t2 .
A net N is an occurrence net if
– for all p ∈ P , |• p| ≤ 1
18 PNSE’18 – Petri Nets and Software Engineering
– F ∗ is a partial order on P ∪ T
– for all x ∈ P ∪ T , the set {y ∈ P ∪ T | yF ∗ x} is finite
– for all x ∈ P ∪ T , x#x does not hold
We will say that two elements x and y of N are concurrent, and write x k y, if
they are not ordered by F ∗ , and they are not in conflict.
By min(N ) we will denote the set of minimal elements with respect to the
partial order induced by F ∗ .
An occurrence net can be used to represent, as a single object, the set of
potential histories of a concurrent system. In particular, an occurrence net can
represent the set of potential histories of an elementary net system.
A B-cut of N is a maximal set of pairwise concurrent elements of P . B-cuts
represent potential global states through which a process can go in a history of
the system modeled by N . By analogy with net systems, we will sometimes say
that an event e of an occurrence net is enabled at a B-cut γ if • e ⊆ γ.
A branching process of Σ = (P, T, F, m0 ) is an occurrence net N = (B, E, F ),
together with a labelling function λ : B ∪ E → P ∪ T , such that
– λ(B) ⊆ P and λ(E) ⊆ T
– for all e ∈ E, the restriction of λ to • e is a bijection between • e and • λ(e);
the same holds for e•
– the restriction of λ to min(N ) is a bijection between min(N ) and m0
– for all e1 , e2 ∈ E, if • e1 = • e2 and λ(e1 ) = λ(e2 ), then e1 = e2
Given two branching processes of Σ, (N1 , λ1 ) and (N2 , λ2 ), we say that (N1 , λ1 )
is a prefix of (N2 , λ2 ) if N1 is a subnet of N2 , and
– min(N1 ) = min(N2 )
– if b ∈ B1 and (e, b) ∈ F2 , then e ∈ E1
– if e ∈ E1 , and b is either a precondition or a postcondition of e in N2 , then
b ∈ B1
For any elementary net system Σ, there exists a unique, up to isomorphism,
maximal branching process of Σ. We will call it the unfolding of Σ, and denote
it by unf(Σ) (see [3]).
A run of Σ is a branching process describing a particular history, in which
conflicts have been solved. A run is a branching process (N, λ) such that the
conflict relation # is empty on its set of elements.
From an initial sequence of an elementary net system Σ, we can derive a run,
which will be a prefix of the unfolding. Informally, given an initial sequence σ,
the corresponding run is obtained starting with the initial B-cut of the unfolding
of Σ, and adding occurrences of the transitions in σ, together with occurrences
of their post-conditions. Two initial sequences that differ only in the order of
concurrent transitions generate the same run. By [σ] we denote the set of initial
sequences that generate the same run as σ.
Let Γ be the set of B-cuts of an occurrence net N = (B, E, F ). A partial
order on Γ can be defined as follows: let γ1 , γ2 be two B-cuts. We say γ1 < γ2 iff
Bernardinello et.al.: Checking Weak Observable Liveness with Games 19
Fig. 1. An example of elementary net system
1. ∀y ∈ γ2 ∃x ∈ γ1 : xF ∗ y
2. ∀x ∈ γ1 ∃y ∈ γ2 : xF ∗ y
3. ∃x, y ∈ γ1,2 : xF + y
In words, γ1 < γ2 if any condition in the second B-cut is or follows a condition of
the first B-cut and any condition in the first B-cut is or comes before a condition
of the second B-cut (and there exists at least one condition coming before).
A sequence of B-cuts, γ0 γ1 . . . γi . . . is increasing if γi < γi+1 for all i ≥ 0.
We will say that an event e ∈ E precedes a B-cut γ, and write e < γ, iff
there is y ∈ γ such that eF + y. In this case, each element of γ either follows e or
is concurrent with e in the partial order given by the unfolding.
Example 1. In Fig. 1 we show an example of elementary net system and Fig. 2
exhibits its unfolding. The set of grey places and transitions and their relations
are an example of run.
2.2 Weak Observable Liveness
In this section we recall the notion of weak observable liveness, first described
in [1] as a variant of observable liveness as introduced in [2].
Let Σ = (P, T, F, m0 ) be an elementary net system. Suppose that Σ models
a User interacting with an environment (called System from now on). Direct
interactions happen by means of a subset of controllable events; whenever such
20 PNSE’18 – Petri Nets and Software Engineering
Fig. 2. The unfolding of the net in Fig. 1
an event is enabled, the User can decide whether trying to fire it or not. If a
controllable event is in conflict with an uncontrollable event, then the User has
no guarantee to ‘win’ the conflict.
In the general setting, we assume that some uncontrollable events are not
observable by the User. Formally, let O ⊆ T be the set of observable transitions
and C ⊆ O be the set of controllable transitions.
Informally, a target transition is weakly observably live (wol) if the User
can use the controllable transitions to force the target to fire infinitely often.
In order to reach the goal, the User decides which controllable transition to
fire on the basis of what he has observed. A response function ϕ : O∗ → 2C
formally describes the behavior of the User: based on the observable transitions
fired in the past, it gives a subset of controllable transitions among which the
User chooses which one to fire next, if possible.
Given a transition sequence σ, σ denotes the projection of σ on O, σ denotes
the projection of σ on C.
Let σ = t1 , t2 , . . . , ti , . . . be an infinite transition sequence enabled at m0 , i.e.:
m0 [t1 im1 [t2 i . . . mi−1 [ti i . . . , and let t be a transition. We call t finally postponed
in σ if there is a prefix from which it is always enabled but never fired, i.e.:
∃j ≥ 0 : ∀k ≥ j : mk [ti ∧ tk 6= t. If t is not finally postponed, we call σ weakly
fair with respect to t. A finite transition sequence is weakly fair with respect to
Bernardinello et.al.: Checking Weak Observable Liveness with Games 21
any transition. We call t finally eligible in σ if there is a prefix from which it is
always suggested by the response function, i.e.: ∃j ≥ 0 : ∀k ≥ j : t ∈ ϕ(σk ).
Definition 1. Let ϕ be a response function. A transition sequence σ is consis-
tent with ϕ if and only if:
1. σ is weakly fair with respect to T \ C
2. ∀σk t if t ∈ C then t ∈ ϕ(σk )
3. if σ is finite, there are no controllable transitions both finally postponed and
finally eligible in σ.
We will refer to the second condition of consistence when we write that an initial
sequence respects a response function.
An observable transition t ∈ O, called target, is weakly observable live, shortly
wol, if and only if there exists a response function ϕ such that t occurs infinitely
often in each maximal transition sequence that is consistent with ϕ.
In this paper, we will consider only elementary nets such that any transition
is observable: O = T . A controlled elementary net system is an elementary net
system with a set C ⊆ T of controllable transitions:
Σ = (P, T, F, m0 , C)
We represent non controllable transitions with empty boxes and the controllable
ones with black boxes.
Example 2. Consider the net shown in Fig. 3, where t7 is the target transition.
Intuitively, to keep t7 alive, at each iteration the User should wait for the System
to choose between t3 and t4 : if t3 fires then the User will fire t1 ; if instead t4 fires
then the User will fire t2 . In such a way, either t5 or t6 can fire, and t7 will occur.
Formally, each transition sequence σ1 that ends with t3 is associated to t1 , i.e.:
ϕ(σ1 ) = {t1 }, and each transition sequence σ2 that ends with t4 is associated to
t2 , i.e.: ϕ(σ2 ) = {t2 }. Notice that t7 is not live according to the classical notion
of liveness. In fact, from the reachable marking {p4 , p5 } no transition can fire.
Fig. 5 shows a run bringing the net to a deadlock. On the other hand, t6 is not
WOL: intuitively, we cannot ensure that the System will fire t4 .
2.3 Canonical Response Function
In this section we introduce a new notion of canonical response function and
show that for every response function there is an “equivalent” canonical function.
Intuitively, if two initial sequences lead to the same B-cut in the unfolding, there
is no reason to give different choices for the two sequences. Hence we introduce
the notion of weakly coherent response function, together with some auxiliary
definitions.
A response function is coherent if it associates to all transition sequences
reaching the same marking the same controllable transitions. A response function
is weakly coherent if it associates to all transition sequences reaching the same
22 PNSE’18 – Petri Nets and Software Engineering
Fig. 3. t7 is wol whereas t6 is not wol
Fig. 4. The unfolding of the net in Fig 3
Bernardinello et.al.: Checking Weak Observable Liveness with Games 23
Fig. 5. A deadlock run of the net in Fig. 3
B-cut in unf(Σ) the same controllable transitions. We will call well-formed a
response function ϕ such that for every initial sequence σ, ϕ(σ) is a subset of the
controllable transitions enabled in m(σ), and ϕ(σ) is non-empty only if, for each
prefix σk t of σ with t ∈ C, t ∈ ϕ(σk ). We will call singular a response function
which associates at most one controllable transition to any transition sequence.
Lemma 1. Let ϕ be a well-formed response function. Then there is at least one
initial sequence that is consistent with ϕ.
Proof. Consider the initial sequence σ = w1 c1 w2 c2 . . . , built as follows:
m0 [w1 im(w1 )[c1 im(w1 c1 )[w2 im(w1 c1 w2 )[c2 im(w1 c1 w2 c2 ) . . .
where, for all k, wk is a sequence of uncontrollable transitions obtained as a
linearization of a maximal step enabled at the preceding marking, m(w1 . . . ck−1 ),
while ck is a sequence of controllable transitions ck = tk1 , tk2 , . . . , tkn such that
∀i ≤ n
– tki ∈ ϕ(w1 c1 . . . wk )
– tki ∈ ϕ(w1 c1 . . . wk tk1 tk2 . . . tki−1 )
– @t ∈ ϕ(w1 c1 . . . wk ) : m(w1 c1 . . . wk ck )[ti,
i.e. only controllable transitions eligible by ϕ(w1 c1 . . . wk ) can occur in the se-
quence and tki occurs if it is eligible by ϕ(w1 c1 . . . wk tk1 tk2 . . . tki−1 ). Notice that
any wi and ci could be empty, and all of them are finite.
This sequence σ is maximal with respect to uncontrollable transitions, re-
spects ϕ, and there is no controllable transition finally eligible. Then this initial
sequence is consistent with ϕ. t
u
The following definitions and lemmas show that we can restrict our attention to
well-formed response functions, without loss in generality.
Definition 2. Let ϕ be a response function.
ϕc (σ) = ϕ(σ) ∩ {t | m0 [σim[ti}
Lemma 2. If a transition t is wol by a response function ϕ, then it is wol by
the response function ϕc .
24 PNSE’18 – Petri Nets and Software Engineering
Proof. We show that all and only the initial sequences consistent with ϕ are
consistent with ϕc .
Let σ be an initial sequence consistent with ϕ, we prove that σ satisfies the
consistence conditions from Def. 1 with ϕc .
1. An initial sequence σ is maximal with respect to uncontrollable transitions
independently from the response function.
2. For each prefix σk t of σ if t ∈ C then t ∈ ϕ(σk ). Notice that σk t is a
transition sequence only if t is enabled in the marking m such that m0 [σk im.
Then t ∈ ϕ(σ) ∩ {t | m0 [σim[ti}.
3. If a transition is not finally eligible by ϕ even more so it is not finally
eligible by ϕc .
Let σ be an initial sequence consistent with ϕc , we prove that σ satisfies the
conditions for consistence from Def. 1 for ϕ.
1. An initial sequence σ is maximal with respect to uncontrollable transitions,
independently from the response function.
2. If t ∈ ϕc (σk ) then t is in ϕ(σk ) because ϕc (σk ) ⊆ ϕ(σk ).
3. A transition t that is finally postponed and finally eligible from a prefix
σk on ϕ is finally postponed and finally eligible from the same prefix on ϕc ; in
fact, by definition of finally eligible and postponed, ∀n > k, t ∈ ϕ(σn ) ∧ mn [ti
implies t ∈ ϕc (σn ). By contradiction if a transition is not finally eligible in ϕc
then it is not finally eligible in ϕ. t
u
Notice that finally eligible implies finally postponed in ϕc .
Definition 3. Let ϕ be a response function and ϕc the transformation previously
described.
(
wf ϕc (σ) if ∀σk t prefix of σ, t ∈ C → t ∈ ϕc (σk )
ϕ (σ) =
∅ else
Observe that ϕwf is a well-formed function.
Lemma 3. If a transition t is wol by a response function ϕ, then it is wol by
a well-formed response function.
Proof. Consider the well-formed response function ϕwf : in order to prove this
lemma we show that all and only the initial sequences consistent with ϕc are
consistent with ϕwf .
Let σ be an initial sequence consistent with ϕc , we prove that σ satisfies the
consistence conditions from Def. 1 with ϕwf .
1. Does not depend on ϕc .
2. Because σ is consistent with ϕc , ∀σk t of σ, t ∈ C → t ∈ ϕc (σk ). Then, by
construction, ∀σk t, t ∈ ϕwf (σk ).
3. If there are no controllable transitions finally eligible by ϕc even more so
there is no transition finally eligible by ϕwf , by construction.
Let σ be an initial sequence consistent with ϕwf , we prove that σ satisfies
the consistence conditions from Def. 1 with ϕc .
Bernardinello et.al.: Checking Weak Observable Liveness with Games 25
1. Does not depend on ϕwf .
2. For each prefix of σ, ϕwf (σk ) ⊆ ϕc (σk ). So, if t ∈ ϕwf (σk ) then t ∈ ϕc (σk ).
3. σ respects ϕwf hence ∀σk : ϕwf (σk ) = ϕc (σk ). Moreover if a transition is
not finally eligible by ϕwf then it isn’t by ϕc .
Remeber that all the initial sequences consistent with ϕc are consistent with
ϕ and vice versa, then the lemma is verified. t
u
We now can build a well-formed response function from a generic response func-
tion.
Definition 4. Let ϕ be a well-formed response function.
[
ϕ0 (σ) = ϕ(β)
β∈[σ]
Observe that ϕ0 is a weakly coherent response function.
Lemma 4. If a transition t is wol by a response function ϕ then it is wol by
a weakly coherent response function.
Proof. Consider the weakly coherent response function ϕ0 . Notice that not all
the initial sequences consistent with ϕ are consistent with ϕ0 because a transition
could be finally eligible by ϕ0 but not by ϕ. Anyway we consider neither these
sequences nor the sequences that are consistent with both the response functions.
We simply show that in all the initial sequences that are consistent only with
ϕ0 , the target occurs infinitely often.
An initial sequence can be not consistent with ϕ but consistent with ϕ0 only
due to the second condition of consistence: in fact the first condition does not
depend from the response function and all the transitions finally eligible in ϕ
are still finally eligible by ϕ0 , by construction of ϕ0 . Let σ 0 = σ1 tσ2 be an initial
sequence, where σ1 is a prefix, t is a controllable transition and σ2 is a suffix. This
sequence is not consistent with ϕ, because t ∈ / ϕ(σ1 ). However, by construction
of ϕ0 , ∃σ10 ∈ [σ1 ] : σ10 tσ2 is consistent with ϕ. In this initial sequence the target
occurs infinitely often, in particular it occurs infinitely often in σ2 . Then the
target occurs infinitely often in σ 0 . On the other hand let σ 0 = σ1 t1 σ2 t2 . . . be
an initial sequence consistent with ϕ0 such that t1 ∈ / ϕ(σ1 ), t2 ∈
/ ϕ(σ1 t1 σ2 ) . . . .
This initial sequence is not consistent with ϕ, but there exists an initial sequence
σ 00 ∈ [σ1 t1 σ2 t2 . . . ] consistent with ϕ. Notice that σ 00 and σ 0 have the same
occurrences of transitions but in a different order. Because σ 00 is consistent with
ϕ, it has infinite occurrences of the target, in the same way σ 0 has. t
u
3 An Asynchronous Game on Petri Nets
In this section we define an asynchronous game on unfoldings. The events of the
unfolding of an elementary net system with controlled transitions will inherit
the quality of being controllable or uncontrollable. Plays of this game will allow
26 PNSE’18 – Petri Nets and Software Engineering
for some level of concurrency. We will then define a notion of strategy for the
player who “owns” the controllable events.
Let Σ = (P, T, F, m0 , C) be a controlled elementary net system, where C ⊆ T
is the set of controllable transitions, and N C = T \ C is the set of uncontrollable
transitions. Let unf(Σ) = (B, E, F, λ) be the unfolding of Σ. Define Ec = {e ∈
E | λ(e) ∈ C}, and Enc = E \ Ec , so that Ec is the set of occurrences of
controllable transitions (we will call them controllable events), while Enc is the
set of occurrences of uncontrollable transitions (uncontrollable events). A play
in the game is a run of the unfolding of Σ, together with an increasing sequence
of B-cuts (think of these cuts as of “snapshots” taken during the play). The run
must be maximal with respect to uncontrollable events, and for each event in
the run there must be a cut in the sequence which follows the event.
Definition 5 (Play). A play is a pair (ρ, π), where ρ = (Bρ , Eρ , Fρ ) is a run of
unf(Σ), and π = γ1 γ2 · · · γi · · · is an increasing sequence of B-cuts of unf(Σ),
such that
– for all e ∈ Enc \ Eρ , the net obtained by adding e and its postconditions to ρ
is not a run of unf(Σ)
– for all e ∈ Eρ , there is γi in π such that e < γi
Let σ be an initial sequence of Σ. Then, there is a unique corresponding run of
unf(Σ). This run, denoted by run(σ), is constructed starting from the initial
B-cut of the unfolding (corresponding to m0 ) and adding the occurrences of the
transitions in σ, in the same order.
If σ = t1 t2 · · · ti · · · , then there is a unique sequence of markings m0 m1 m2 · · ·
such that mi−1 [ti imi for all i, and a corresponding unique increasing sequence
of B-cuts cseq(σ) = γ0 γ1 γ2 · · · in the unfolding, with λ(γj ) = mj for all j.
Given σ, we can then define a play play(σ) = (run(σ), cseq(σ))
Vice versa, let (ρ, π) be a play, with π = γ1 γ2 · · · . For any pair γi , γi+1 the
events between γi and γi+1 are partially ordered by F ∗ . Take any linearization
of this partial order and call it σi , then σ1 σ2 · · · is an initial sequence of Σ. We
will refer to any of such sequences as an initial sequence derived from (ρ, π).
In this paper we assume that all transitions (and all events in the unfolding)
are observable by the User. Hence, a strategy can be definied as a map that
associates a controllable event, or the choice to wait, to any B-cut.
Definition 6 (Strategy). Let Γ be the set of B-cuts of unf(Σ). A strategy is
a function α : Γ → 2EC such that |α(γ)| ≤ 1 for all γ ∈ Γ , if α(γ) = {e} then
•
e ⊆ γ, i.e. if e is chosen by α in γ then it is enabled in γ.
The notions of ‘finally eligible’ and ‘finally postponed’, which have been defined
for response functions, can be translated for strategies.
Definition 7 (Finally eligible). Let π = γ0 γ1 . . . γi . . . be an increasing se-
quence of B-cuts and let α be a strategy. The event e is finally eligible in π by
α iff ∃j ≥ 0 : ∀k ≥ j : α(γk ) = {e}.
Bernardinello et.al.: Checking Weak Observable Liveness with Games 27
Definition 8 (Finally postponed). Let π = γ0 γ1 . . . γi . . . be an increasing
sequence of B-cuts. The event e is finally postponed in π iff ∃j ≥ 0 : ∀k ≥ j :
γk [ei, i.e. if e is always enabled but never fire.
We can now state when a play unfolds according to a strategy.
Definition 9 (α-play). Let ρ = (Bρ , Eρ , Fρ ) be a run of unf(Σ), π = γ0 γ1 γ2 . . .
be a strictly increasing sequence of B-cuts and α be a strategy. The pair (ρ, π) is
an α-play iff:
1. ρ is maximal with respect to Enc ,
2. ∀x ∈ Eρ ∩ Ec , ∃γi ∈ π : α(γi ) = {x} ∧ γi+1 = (γi \ • x) ∪ x• , namely if a
controllable event occurs in the run then there exists a B-cut in which the
event is chosen by the strategy and it has fired in the immediately successive
B-cut.
3. ∀x ∈ Eρ ∩ Enc , ∃γi ∈ π such that x comes before γi , namely if a not con-
trollable event occurs in the run then there exists a B-cut in the sequence
resulting from its occurrence,
4. @x ∈ Ec \ Eρ such that it is finally eligible by α and finally postponed in π.
Example 3. We show here an example of strategy on the unfolding in Fig. 4.
We want to ensure that t7 occurs infinitely often in every play. For that, the
User should wait until he observed a B-cut following an occurrence of t3 or t4 .
In particular after a B-cut immediately following an occurrence of t3 he will
choose the enabled occurrence of t1 on the other hand after a B-cut immediately
following an occurrence of t4 he will choose the enabled occurrence of t2 , i.e.
α({p11 , p15 }) = {t11 }, α({p11 , p16 }) = {t12 }, α({p21 , p25 }) = {t21 }, α({p21 , p26 }) = {t22 },
and so on. In any other B-cut γn he will do nothing, i.e. α(γn ) = ∅. In Fig. 6 we
exhibit an α-play. Notice that this strategy has a similar behavior to the response
function in Example 2. Intuitively we should be able to derive a strategy from
a response function, to do it we should associate the B-cut reached by an initial
sequence to the enabled occurrence of the transition suggested by the response
function itself. We formalize this intuition in Section 4.
4 Checking Weak Observable Liveness through Games
In this section we show that the problem of weak observable liveness can be
reformulated on the unfolding of the underlying elementary net system. Response
functions correspond to strategies in the game defined on the unfolding, and a
target transition is wol if, and only if, the User has a winning strategy in the
game. Here, we restrict to singular response functions.
Definition 10. Let Σ = (P, T, F, m0 , C) be a controllable elementary net sys-
tem, and t ∈ T a target transition. A strategy α is winning if in every α-play of
unf(Σ) the set of occurrences of t is infinite.
28 PNSE’18 – Petri Nets and Software Engineering
Fig. 6. α-play on Fig. 4 with the strategy described in Example 3
Let γ ∈ Γ be a B-cut. This B-cut is generated in the unfolding by a run corre-
sponding to a family of initial sequences in the system. These sequences differ
only in the order of concurrent transitions. Let fam(γ) denote the family of
initial sequences that generate the B-cut γ. Let σ be an initial sequence; then
cut(σ) denotes the final cut of run(σ).
From a singular, weakly coherent, well-formed response function ϕ, we derive
a strategy, αϕ . To this end, we exploit a simple fact about unfoldings: if σt is an
initial sequence of Σ, then there is a unique event e in unf(Σ) which maps to t
and is enabled in the cut reached by the run corresponding to σ.
Definition 11. Let ϕ : T ∗ → 2C be a singular, weakly coherent, and well-formed
response function for Σ. Take a B-cut γ in unf(Σ) and any σ ∈ fam(γ). Then
(
{e} if ϕ(σ) = {t} and λ(e) = t and cut(σ)[ei
αϕ (γ) =
∅ if ϕ(σ) = ∅
Since ϕ is weakly coherent, the definition does not depend on the choice of σ.
From a strategy α, we derive a singular, weakly coherent, well-formed response
function, ϕα .
Bernardinello et.al.: Checking Weak Observable Liveness with Games 29
Definition 12. Let α be a strategy for unf(Σ). Take τ , an initial sequence of
Σ, and let γ be the final cut of run(τ ). If γ is reachable by an α-play, define
(
{t} if α(γ) = {e} and λ(e) = t
ϕα (τ ) =
∅ if α(γ) = ∅
If γ is not reachable by any α-play, then define ϕα (τ ) = ∅.
Example 4. We show here how to derive a response function ϕα from the strategy
α that we built in Example 3 (see Fig. 4). By definition, for each B-cut we
need to collect all the initial sequences of the system that generate this B-cut.
Then the response function will associate to these initial sequences the transition
of the system corresponding to the occurrence that the strategy associates to
the B-cut. In the example the B-cuts composed by the occurrence of p1 , p5 are
generated by the initial sequence t3 and all the initial sequences ending with
the transitions t7 t3 . Because all the B-cuts composed by the occurrence of p1 , p5
are associated by α to an occurrence of t1 , ϕα associates t1 to all the initial
sequences σ1 collected before, i.e. ϕα (σ1 ) = {t1 }. Analogously, we collect the
initial sequences σ2 who generates the B-cuts composed by the occurrence of
p1 , p6 . These sequences are t4 and all the initial sequences ending with t7 t4 .
Because these B-cuts are associated to an occurrence of t2 , then ϕα associate
t2 to all the initial sequences collected., i.e. ϕα (σ2 ) = {t2 }. All other initial
sequences σ3 are associated to ∅, i.e. ϕα (σ3 ) = ∅.
The labelling function λ used in the definition of unfolding is in general not
injective. Its restriction to the set of events enabled at a given B-cut is injective.
This allows us to define the following map, which, by abuse of notation, we denote
λ−1 , associated to a singular, weakly coherent, well-formed response function ϕ.
(
−1 ∅ if ϕ(σ) = ∅
λ (ϕ(σ)) = (1)
{x} : λ(x) ∈ ϕ(σ) ∧ cut(σ)[xi, if ϕ(σ) ⊆ T
Note that, if ϕ(σ) ⊆ T , then x exists and is unique, since ϕ is singular, weakly
coherent and well-formed, and a B-cut can enable at most one occurrence of a
given transition.
Lemma 5. Let ϕ be a singular, weakly coherent, well-formed response function.
Then ϕαϕ = ϕ.
Proof. Let ϕ : T ∗ → 2C be a singular, weakly coherent, well-formed response
function. Let γ ∈ Γ be a B-cut. By construction of a strategy from a response
function,
αϕ (γ) = λ−1 (ϕ(σ)) (2)
where σ ∈ fam(γ). Notice that it is immaterial which σ ∈ fam(γ) we choose,
because the response function is weakly coherent. We now derive a response
function from αϕ . Let σ be an initial sequence and let γ = cut(σ).
ϕαϕ (σ) = λ(αϕ (γ)) = λ(λ−1 (ϕ(σ 0 ))) = ϕ(σ 0 ) (3)
30 PNSE’18 – Petri Nets and Software Engineering
where σ 0 ∈ fam(γ). The first equality follows from the construction of a response
function from a strategy, the second from Eq. (2), the third one by reduction of
λ with λ−1 . t
u
Lemma 6. Let α be a strategy. Then αϕα = α.
Proof. Let α : Γ → 2Ec be a strategy and γ a B-cut. By construction of a
strategy from a response function,
αϕα (γ) = λ−1 (ϕα (σ)) (4)
where σ ∈ fam(γ).
Now, replace the derived response function with ϕα .
λ−1 (ϕα (σ)) = λ−1 (λ(α(cut(σ))) (5)
Remember that σ is an element of fam(γ), so cut(fam(γ)) is simply γ. By
definition, we now have
λ−1 (λ(α(cut(σ))) = α(γ) (6)
t
u
Proposition 1. Let ϕ be a singular, weakly coherent and well-formed response
function, and let αϕ be the strategy derived by ϕ. Let σ be an initial sequence
consistent with ϕ. Then (run(σ), cseq(σ)) is an αϕ -play.
Proof. In order to show that (run(σ), cseq(σ)) is an αϕ -play we have to verify
the clauses in Def. 9. Put ρ = run(σ), and π = cseq(σ).
1. We proceed by contradiction. Suppose that ρ is not maximal with respect
to Enc . That means that there is at least a non-controllable event e which is
enabled after a prefix of π. However, by construction of π, if this event exists
then an enabled and non-controllable transition t exists and it doesn’t fire in the
original system Σ. This means that σ is not a weakly fair initial sequence with
respect to uncontrollable transitions. This is a contradiction with the hypothesis,
so ρ is a maximal run with respect to Enc .
2. By the definition of consistence, if ti ∈ σ ∩ C then ti ∈ ϕ(σi−1 ). Let γi−1
be the B-cut generated by the prefix σi−1 , by construction of αϕ , ϕ(σi−1 ) =
λ(αϕ (γi−1 )). Therefore, by construction of π, γi is the B-cut following the occur-
rence of ei , where λ(ei ) = ti , and because of the firing rule γi = (γi−1 \ • ei ) ∪ ei • .
3. Remember that, by construction of ρ, an event occurs in ρ if and only if it
is in the initial sequence σ. So the condition is verified by construction of π, in
0
fact ∀ei the prefix σi−1 ei generates the B-cut γi and γi follows the occurrence
of ei .
4. We proceed by contradiction. Let e ∈ Ec be finally postponed and finally
eligible in (ρ, π). By construction of π, e must be finally postponed in σ. Likewise,
by construction of αϕ , an event finally eligible by αϕ is finally eligible by ϕ in
σ. In fact, ∀σi , ϕ(σi ) = λ(αϕ (γi )). So, if such an e exists, then λ(e) is finally
postponed and finally eligible by ϕ on σ, which contradicts the hypothesis that
σ is consistent with ϕ. t
u
Bernardinello et.al.: Checking Weak Observable Liveness with Games 31
Proposition 2. Let ϕ be a singular, weakly coherent, and well-formed response
function, and let αϕ be the strategy derived by ϕ. Any initial sequence σ derived
from an αϕ -play (ρ, π) is consistent with ϕ.
Proof. In order to show that σ is consistent with ϕ we have to verify the clause
in Def. 1:
1. We prove this by contradiction. Remember that the run ρ is maximal with
respect to Enc and for this reason there is no event e ∈ Enc enabled thereafter a
prefix of π. Suppose that an initial sequence σ, with a non controllable transition
t enabled after a prefix, exists. Then, because σ is derived by the cut sequence
π, an occurrence of t in π is also enabled thereafter a prefix of π. This means
that ρ is not maximal with respect to Enc . By contradiction, σ is weakly fair
with respect to uncontrollable transitions.
2. By definition of π, for every occurrence e of a controllable transition t
which occurs in the run, there is a B-cut γj in which e is enabled and chosen
by αϕ , i.e. αϕ (γj ) = e, and an immediately following B-cut γj+1 in which e has
fired. Because σ generates the sequence π, the B-cuts γj and γj+1 are generated
by the prefixes σi−1 and σi−1 ti , where ti = λ(e) is a controllable transition. In
particular, by construction of the derived strategy, λ(αϕ (γj )) = ϕ(σi−1 ) = ti ,
and this verifies the properties.
3. We proceed by contradiction. Suppose that an initial sequence σ exists,
with σ such that it has a finally eligible and finally postponed controllable transi-
tion, i.e. such that ϕ(σi ) = ϕ(σi+1 ) = ϕ(σi+2 ) = · · · = {t}. Let σi+n1 , σi+n2 , . . .
be the prefixes generating the B-cuts of π : γj , γj+1 , . . . following the occur-
rence of σi in the unfolding. For all these B-cuts there is an event e such
that λ(e) = t, e is enabled and eligible by αϕ . In fact, by construction of αϕ ,
λ(αϕ (γj )) = ϕ(σi+n1 ) = t. This means that the controllable occurrence e is fi-
nally eligible in π, which is a contradiction. t
u
Proposition 3. Let α be a strategy and let ϕα be the response function derived
from α. Any initial sequence σ derived from an α-play (ρ, π) is consistent with
ϕα .
Proof. This proposition is a direct consequence of Lemma 6 and Proposition
2. t
u
Proposition 4. Let α be a strategy and let ϕα be the response function derived
from α. Let σ be an initial sequence consistent with ϕ. Then (run(σ), cseq(σ))
is an α-play.
Proof. This proposition is a direct consequence of Lemma 6 and Proposition
1. t
u
The four propositions in this section show that the problem of weak observable
liveness of a transition t in system Σ can be equivalently faced either looking for
a response function or for a strategy on unf(Σ). This is more formally stated in
the following corollaries.
32 PNSE’18 – Petri Nets and Software Engineering
Corollary 1. Let α be a winning strategy for a transition t on the unfolding of
an elementary net system Σ. Then t is wol in Σ by the response function ϕα
derived from α.
Corollary 2. Let ϕ be a singular and weakly coherent response function showing
that t is wol in Σ. Then the derived strategy αϕ is a winning strategy for t on
unf(Σ).
5 Conclusion
We have defined a type of asynchronous game for elementary net systems. The
game is actually played on the unfolding of the given net system Σ. Each event
of the unfolding is assigned to one of two players, User and System, on the basis
of a partition of the transitions of Σ. The game is asynchronous in the sense
that its plays are runs in the unfolding, with a partial order on events.
We have shown that the problem of weak observable liveness can be trans-
lated into an equivalent problem on the unfolding of an elementary net system,
and can be solved by looking for a winning strategy for the User in the associated
game.
In this paper we have imposed some restrictions, the most stringent of which
is the assumptions that all transitions are observable by the User.
The immediate developments of this work will follow two main directions.
The first consists in considering partial observability of transitions. This makes
the problem harder because the projection of an initial sequence on observable
transitions does not uniquely determine the final marking, and the final B-cut
in the unfolding. The second directions will deal with the search for algorithms
to compute a winning strategy, if such a strategy exists. We plan to tackle the
problem looking for an adequate notion of complete finite prefix of the unfolding.
Further developments concern the extension of the idea to Place/Transition
nets and to coloured nets. Apart from the problem of weak observable liveness,
we will investigate the application of the game defined in this paper to other
classes of problems.
References
1. Luca Bernardinello, Görkem Kilinç, and Lucia Pomello. Weak observable liveness
and infinite games on finite graphs. In Wil M. P. van der Aalst and Eike Best,
editors, Application and Theory of Petri Nets and Concurrency - 38th International
Conference, PETRI NETS 2017, Zaragoza, Spain, June 25-30, 2017, Proceedings,
volume 10258 of Lecture Notes in Computer Science, pages 181–199. Springer,
2017.
2. Jörg Desel and Görkem Kilinç. Observable liveness of petri nets. Acta Inf., 52(2-
3):153–174, 2015.
3. Joost Engelfriet. Branching processes of petri nets. Acta Inf., 28(6):575–591, 1991.
4. Bernd Finkbeiner and Paul Gölz. Synthesis in distributed environments. CoRR,
abs/1710.05368, 2017.
Bernardinello et.al.: Checking Weak Observable Liveness with Games 33
5. Bernd Finkbeiner and Ernst-Rüdiger Olderog. Petri games: Synthesis of distributed
systems with causal memory. In Adriano Peron and Carla Piazza, editors, Pro-
ceedings Fifth International Symposium on Games, Automata, Logics and Formal
Verification, GandALF 2014, Verona, Italy, September 10-12, 2014., volume 161
of EPTCS, pages 217–230, 2014.
6. Julian Gutierrez. Concurrent logic games on partial orders. In Lev D. Beklemishev
and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computa-
tion - 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May
18-20, 2011. Proceedings, volume 6642 of Lecture Notes in Computer Science, pages
146–160. Springer, 2011.
7. Paul-André Melliès and Samuel Mimram. Asynchronous games: Innocence without
alternation. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR
2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lis-
bon, Portugal, September 3-8, 2007, Proceedings, volume 4703 of Lecture Notes in
Computer Science, pages 395–411. Springer, 2007.
8. Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of
the IEEE, 77(4):541–580, April 1989.
9. Grzegorz Rozenberg and Joost Engelfriet. Elementary net systems. In Wolfgang
Reisig and Grzegorz Rozenberg, editors, Lectures on Petri Nets I: Basic Models,
Advances in Petri Nets, the volumes are based on the Advanced Course on Petri
Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer
Science, pages 12–121. Springer, 1996.
10. Glynn Winskel. Distributed games and strategies. CoRR, abs/1607.03760, 2016.
34 PNSE’18 – Petri Nets and Software Engineering