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