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