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. 2
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 2 P [ T be an element of the net, the pre-set of x is the set x = fy 2 P [ T j (y; x) 2 F g, the post-set of x is the set x = fy 2 P [ T j (x; y) 2 F g. We assume that any transition has non-empty pre-set and post-set: 8t 2 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 0 P , T 0; T , and F 0 is F restricted to the elements in N 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 n t, denoted m[tim0.
Two transitions, t1 and t2, are independent if ( t1 [ t1) and ( t2 [ t2) are disjoint. A step at a marking m is a set of pairwise independent transitions, all enabled at m.
A sequence of transitions = t1t2t3 : : : - finite or not - is enabled at m if m[t1im1[t2im2[t3i : : : . 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 2 N : i < j j; then t1t2 : : : 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 [m0i.
Let 2 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 2 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 2 P [ T are said to be in conflict, denoted x#y, iff there exist t1; t2 2 T : t1 6= t2; t1F x; t2F y ^ 9p 2 t1 \ t2.
– for all p 2 P , j pj – F is a partial order on P [ T – for all x 2 P [ T , the set fy 2 P [ T j yF xg is finite – for all x 2 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 2 E, the restriction of to e is a bijection between e and the same holds for e – the restriction of to min(N ) is a bijection between min(N ) and m0 – for all e1; e2 2 E, if e1 = e2 and (e1) = (e2), then e1 = e2 (e); 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 2 B1 and (e; b) 2 F2, then e 2 E1 – if e 2 E1, and b is either a precondition or a postcondition of e in N2, then b 2 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 order on be the set of B-cuts of an occurrence net N = (B; E; F ). A partial can be defined as follows: let 1; 2 be two B-cuts. We say 1 < 2 iff 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; 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 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[t1im1[t2i : : : mi 1[tii : : : , 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.: 9j 0 : 8k 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 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.: 9j 0 : 8k j : t 2 '( k). Definition 1. Let ' be a response function. A transition sequence tent with ' if and only if: is consis1. is weakly fair with respect to T n C 2. 8 kt if t 2 C then t 2 '( k)
We will refer to the second condition of consistence when we write that an initial sequence respects a response function.
An observable transition t 2 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.:
'(
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. 4. The unfolding 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 kt of with t 2 C, t 2 '( k). We will call singular a response function which associates at most one controllable transition to any transition sequence.
Proof. Consider the initial sequence
= w1c1w2c2 : : : , built as follows: m0[w1im(w1)[c1im(w1c1)[w2im(w1c1w2)[c2im(w1c1w2c2) : : : 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 = t1k; t2k; : : : ; tkn such that 8i n – tik 2 '(w1c1 : : : wk) – tik 2 '(w1c1 : : : wkt1kt2k : : : tik 1) – @t 2 '(w1c1 : : : wk) : m(w1c1 : : : wkck)[ti, i.e. only controllable transitions eligible by '(w1c1 : : : wk) can occur in the sequence and tik occurs if it is eligible by '(w1c1 : : : wkt1kt2k : : : tik 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, respects ', and there is no controllable transition finally eligible. Then this initial sequence is consistent with '. tu The following definitions and lemmas show that we can restrict our attention to well-formed response functions, without loss in generality.
'c( ) = '( ) \ ft j m0[ im[tig
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 kt of if t 2 C then t 2 '( k). Notice that kt is a transition sequence only if t is enabled in the marking m such that m0[ kim. Then t 2 '( ) \ ft j m0[ im[tig.
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 2 '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, 8n > k; t 2 '( n) ^ mn[ti implies t 2 'c( n). By contradiction if a transition is not finally eligible in 'c then it is not finally eligible in '. tu 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 ; else
8 kt prefix of ; t 2 C ! t 2 'c( k) Observe that 'wf is a well-formed function.
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, 8 kt of ; t 2 C ! t 2 'c( k). Then, by construction, 8 kt; t 2 '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. 1. Does not depend on 'wf . 2. For each prefix of , 'wf ( k) 'c( k). So, if t 2 'wf ( k) then t 2 'c( k). 3. respects 'wf hence 8 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. tu We now can build a well-formed response function from a generic response function.
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 = 1t 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 2= '(
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; m0; C) be a controlled elementary net system, where C T is the set of controllable transitions, and N C = T n C is the set of uncontrollable transitions. Let unf( ) = (B; E; F; ) be the unfolding of . Define Ec = fe 2 E j (e) 2 Cg, and Enc = E n 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 2 Enc n E , the net obtained by adding e and its postconditions to is not a run of unf( ) – for all e 2 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 = t1t2 ti , then there is a unique sequence of markings m0m1m2 such that mi 1[tiimi 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.
a function : ! 2EC such that j ( )j 1 for all 2 , if ( ) = feg 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 sequence of B-cuts and let be a strategy. The event e is finally eligible in by iff 9j 0 : 8k j : ( k) = feg. Definition 8 (Finally postponed). Let = 0 1 : : : i : : : be an increasing sequence of B-cuts. The event e is finally postponed in iff 9j 0 : 8k 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:
2. 8x 2 E \ Ec; 9 i 2 : ( i) = fxg ^ i+1 = ( i n 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. 8x 2 E \ Enc; 9 i 2 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 2 Ec n 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.
(fp11; p15g) = ft11g; (fp11; p16g) = ft21g; (fp12; p25g) = ft12g; (fp21; p26g) = ft22g; 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
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 system, and t 2 T a target transition. A strategy is winning if in every -play of unf( ) the set of occurrences of t is infinite. Let 2 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 ! 2C be a singular, weakly coherent, and well-formed response function for . Take a B-cut in unf( ) and any 2 fam( ). Then and (e) = t and cut( )[ei
From a strategy , we derive a singular, weakly coherent, well-formed response function, ' . 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 and (e) = t 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 t7t3. 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. ' (
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 '( ) = ; fxg : (x) 2 '( ) ^ 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.
Then ' ' = '.
! 2C be a singular, weakly coherent, well-formed response
be a B-cut. By construction of a strategy from a response
Proof. Let ' : T
function. Let
function,
2
where 2 fam( ). Notice that it is immaterial which 2 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( ).
' ' ( ) = ( '( )) = (
(
be a strategy. Then ' = .
Proof. Let : ! 2Ec be a strategy and strategy from a response function, a B-cut. By construction of a where 2 fam( ).
Now, replace the derived response function with ' .
1(' ( )) = 1( ( (cut( ))) Remember that is an element of fam( ), so cut(fam( )) is simply . By definition, we now have
1( ( (cut( ))) = ( )
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 2 \ C then ti 2 '( 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 ei, where (ei) = ti, and because of the firing rule i = ( i 1 n 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 fact 8ei the prefix i0 1ei generates the B-cut i and i follows the occurrence of ei.
4. We proceed by contradiction. Let e 2 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, 8 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 '.
(
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 2 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 1ti, 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 transition, i.e. such that '( i) = '( i+1) = '( i+2) = = ftg. Let i+n1 ; i+n2 ; : : : 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.
Proof. This proposition is a direct consequence of Lemma 6 and Proposition 2.
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. tu 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.
an elementary net system . Then t is wol in by the response function ' derived from .
that t is wol in . Then the derived strategy ' is a winning strategy for t on unf( ). 5
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.