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.
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 derived 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 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 described 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 definitions. 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.
In this section we collect basic definitions and facts about Petri nets and weak observable liveness.
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
We assume that any transition has non-empty pre-set and post-set:
A subnet of N = (P, T, F ) is an elementary net N = (P , T , F ) such that P ⊆ P , T , ⊆ T , and F is F restricted to the elements in N .
An elementary net system is a quadruple Σ = (P, T, F, m 0 ) consisting of a finite elementary net N = (P, T, F ) and an initial marking m 0 ⊆ P . A marking is a subset of P and it represents a global state.
Two transitions, t 1 and t 2 , are independent 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 t 1 t 2 . . . t i is called prefix of σ, denoted by σ i . If σ is finite and enabled at m then we write m[σ m n and say that m n is reachable from m. The set of reachable markings of an elementary net system is the set of markings reachable from the initial marking m 0 , denoted [m 0 .
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( ) = m 0 .
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 t 1 , t 2 ∈ T :
-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 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
A branching process of Σ = (P, T, F, m 0 ) 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 m 0 for all e 1 , e 2 ∈ E, if • e 1 = • e 2 and λ(e 1 ) = λ(e 2 ), then e 1 = e 2 Given two branching processes of Σ, (N 1 , λ 1 ) and (N 2 , λ 2 ), we say that 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 Fig. 1. An example of elementary net system
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.
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, m 0 ) 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 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 * → 2 C 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 σ = t 1 , t 2 , . . . , t i , . . . be an infinite transition sequence enabled at m 0 , i.e.:
. . , 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 : m k [t ∧ t k = 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 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 consistent with ϕ if and only if:
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:
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 t 7 is the target transition. Intuitively, to keep t 7 alive, at each iteration the User should wait for the System to choose between t 3 and t 4 : if t 3 fires then the User will fire t 1 ; if instead t 4 fires then the User will fire t 2 . In such a way, either t 5 or t 6 can fire, and t 7 will occur. Formally, each transition sequence σ 1 that ends with t 3 is associated to t 1 , i.e.: ϕ(σ 1 ) = {t 1 }, and each transition sequence σ 2 that ends with t 4 is associated to t 2 , i.e.: ϕ(σ 2 ) = {t 2 }. Notice that t 7 is not live according to the classical notion of liveness. In fact, from the reachable marking {p 4 , p 5 } no transition can fire. Fig. 5 shows a run bringing the net to a deadlock. On the other hand, t 6 is not WOL: intuitively, we cannot ensure that the System will fire t 4 .
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 Fig. 3. t7 is wol whereas t6 is not wol Fig. 4. The unfolding of the net in Fig 3 22 PNSE'18 -Petri Nets and Software Engineering 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 σ = w 1 c 1 w 2 c 2 . . . , built as follows:
where, for all k, w k is a sequence of uncontrollable transitions obtained as a linearization of a maximal step enabled at the preceding marking, m(w
i.e. only controllable transitions eligible by ϕ(w 1 c 1 . . . w k ) can occur in the sequence and t k i occurs if it is eligible by ϕ(w
). Notice that any w i and c i could be empty, and all of them are finite.
This sequence σ is maximal with respect to uncontrollable transitions, respects ϕ, and there is no controllable transition finally eligible. Then this initial sequence is consistent with ϕ.
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.
If a transition t is wol by a response function ϕ, then it is wol by the response function ϕ c . 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
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
3. A transition t that is finally postponed and finally eligible from a prefix σ k on ϕ is finally postponed and finally eligible from same prefix on ϕ c ; in fact, by definition of finally eligible and postponed, ∀n > k, t ∈ ϕ(σ n ) ∧ m n [t implies t ∈ ϕ c (σ n ). By contradiction if a transition is not finally eligible in ϕ c then it is not finally eligible in ϕ.
Notice that finally eligible implies finally postponed in ϕ c . Definition 3. Let ϕ be a response function and ϕ c the transformation previously described.
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 .
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.
We now can build a well-formed response function from a generic response function.
Definition 4. Let ϕ be a well-formed response function.
Observe that ϕ 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 ϕ . Notice that not all the initial sequences consistent with ϕ are consistent with ϕ because a transition could be finally eligible by ϕ 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 ϕ , the target occurs infinitely often.
An initial sequence can be not consistent with ϕ but consistent with ϕ 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 ϕ , by construction of ϕ . Let σ = σ 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 ϕ , ∃σ 1 ∈ [σ 1 ] : σ 1 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 σ . On the other hand let σ = σ 1 t 1 σ 2 t 2 . . . be an initial sequence consistent with ϕ such that t 1 / ∈ ϕ(σ 1 ), t 2 / ∈ ϕ(σ 1 t 1 σ 2 ) . . . . This initial sequence is not consistent with ϕ, but there exists an initial sequence σ ∈ [σ 1 t 1 σ 2 t 2 . . . ] consistent with ϕ. Notice that σ and σ have the same occurrences of transitions but in a different order. Because σ is consistent with ϕ, it has infinite occurrences of the target, in the same way σ has.
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 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, m 0 , 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 E c = {e ∈ E | λ(e) ∈ C}, and E nc = E \ E c , so that E c is the set of occurrences of controllable transitions (we will call them controllable events), while E nc 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 ρ
for all e ∈ E nc \ 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 m 0 ) and adding the occurrences of the transitions in σ, in the same order.
If
for all i, and a corresponding unique increasing sequence of B-cuts cseq(σ) = γ 0 γ 1 γ 2 • • • in the unfolding, with λ(γ j ) = m j 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.
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 sequence of B-cuts and let α be a strategy. The event e is finally eligible in π by α iff ∃j ≥ 0 : ∀k ≥ j : α(γ k ) = {e}. 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 [e , 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:
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 ρ ∩ E nc , ∃γ i ∈ π such that x comes before γ i , namely if a not controllable event occurs in the run then there exists a B-cut in the sequence resulting from its occurrence, 4.
x ∈ E c \ 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 t 7 occurs infinitely often in every play. For that, the User should wait until he observed a B-cut following an occurrence of t 3 or t 4 . In particular after a B-cut immediately following an occurrence of t 3 he will choose the enabled occurrence of t 1 on the other hand after a B-cut immediately following an occurrence of t 4 he will choose the enabled occurrence of t 2 , i.e. α({p 1 1 , p
2 }, 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.
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, m 0 , C) be a controllable elementary net system, and t ∈ T a target transition. A strategy α is winning if in every α-play of unf(Σ) the set of occurrences of t is infinite. Let γ ∈ Γ be a B-cut. This B-cut is generated in the unfolding by a run corresponding 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 * → 2 C be a singular, weakly coherent, and well-formed response function for Σ. Take a B-cut γ in unf(Σ) and any σ ∈ fam(γ). Then
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, ϕ α .
where σ ∈ 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 .
Lemma 6. Let α be a strategy. Then α ϕα = α.
Proof. Let α : Γ → 2 Ec be a strategy and γ a B-cut. By construction of a strategy from a response function,
where σ ∈ fam(γ). Now, replace the derived response function with ϕ α .
Remember that σ is an element of fam(γ), so cut(fam(γ)) is simply γ. By definition, we now have
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 E nc . 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 E nc .
2. By the definition of consistence, if t i ∈ σ ∩ C then t i ∈ ϕ(σ 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 occurrence of e i , where λ(e i ) = t i , and because of the firing rule γ i = (γ i−1 \ • e i ) ∪ e i • . 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 fact ∀e i the prefix σ i−1 e i generates the B-cut γ i and γ i follows the occurrence of e i .
4. We proceed by contradiction. Let e ∈ E c 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 ϕ.
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(Σ).
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 translated 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.
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
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 p 1 , p 5 are generated by the initial sequence t 3 and all the initial sequences ending with the transitions t 7 t 3 . Because all the B-cuts composed by the occurrence of p 1 , p 5 are associated by α to an occurrence of t 1 , ϕ α associates t 1 to all the initial sequences σ 1 collected before, i.e. ϕ α (σ 1 ) = {t 1 }. Analogously, we collect the initial sequences σ 2 who generates the B-cuts composed by the occurrence of p 1 , p 6 . These sequences are t 4 and all the initial sequences ending with t 7 t 4 . Because these B-cuts are associated to an occurrence of t 2 , then ϕ α associate t 2 to all the initial sequences collected., i.e.
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 ϕ.
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 * → 2 C be a singular, weakly coherent, well-formed response function. Let γ ∈ Γ be a B-cut. By construction of a strategy from a response function,
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(σ).
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 E nc and for this reason there is no event e ∈ E nc 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 E nc . 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 t i , where t i = λ(e) is a controllable transition. In particular, by construction of the derived strategy, λ(α ϕ (γ j )) = ϕ(σ i−1 ) = t i , 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 transition, i.e. such that ϕ(σ
. . be the prefixes generating the B-cuts of π : γ j , γ j+1 , . . . following the occurrence 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 finally eligible in π, which is a contradiction. 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.
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.
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.