Whereas the traditional liveness property for Petri nets guarantees 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 controllable transitions. We introduce observable liveness and show this new notion generalizes liveness in the following sense: liveness of a net implies 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.
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. [
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 [
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.
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 vending 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 observed 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
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 conditions 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.
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 occurrence 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.
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
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 m0(p) = 8 < m(p) + 1 m(p) 1 : m(p) if p 2 t•, p 2 / •t if p 2 •t, p 2 / t• otherwise We denote this by m ! t 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 [m 2 R(N ) ^ m ! t 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.
If m1! t1 m2! t2 m3! t3 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. Equivalently, 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 transitions 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 [
In order to give the definition of observable liveness, we first stick to observable 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 controllable 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.
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
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:
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.
fair w.r.t. all controllable transitions t satisfying t 2 / ' ( 0 0) for only finitely many prefixes 0of .
belong to ' ( 0 ) (this includes deadlocks).
occurrence sequence enabled at m. If = 1 2 and m! 1 m1, then 2 is a ' -maximal occurrence sequence enabled at m1. Proof. The claim follows immediately from the definition of ' -maximal occurrence sequence. tu
Some comments: All i in Definition 1 are finite and succeeded by a controllable 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 controllable 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. 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.
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:
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.
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. So assume observable liveness of t, i.e., a response function ' t : O⇤ ! 2C 00 such that, for each m0! m0, each ' t-maximal occurrence sequence enabled at m0 contains an occurrence of t (notice that we replaced 0 by 00 and m by 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 m!0 0 1 m1 for some marking m1. This marking m1 enables the ' t-maximal 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. tu 5
In this section, we provide some properties of observable liveness and relations to traditional liveness.
Lemma 2. For each response function ' and each m0! maximal occurrence sequence enabled at m. 0 m, there is a ' Proof. In order to construct a ' -maximal occurrence sequence, we proceed iteratively. 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.
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.
tu tu tu
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 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 coincides 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 0t
Let 0 0 t = 0 0t = t1t2t3 . . . tk and m!0 . We choose any response function with ' t(t1t2 . . . 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.
Corollary 2. If O = C = T , then observable liveness of a net coincides with liveness of the net.
that m0! the sequence 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 0 m! m0 ! has to include t to be observably live. Since does not include any instance of t, t cannot be observably live.
6
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 unobservable 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 setting; the automated part of a system often behaves deterministically (but still concurrently), whereas the user model might allow for alternatives. tu tu tu tu
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 [
able marking m enabling u, every other transition v enabled at m is concurrent to u, i.e., •u \ •v = ; .
marking m, such that •u \ •v = ; . Then m enables u v as well as v u, and both sequences lead to the same marking.
A well-known result for conflict-free nets [
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 0 u. Let m ! v 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 .
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.
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 m ! v 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. tu
The following theorem constitutes the main result of this paper. It applies only to nets where the only possible conflicts occur between controllable transitions, 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.
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 transition 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 occurrences 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.
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.
t and an occurrence sequence enabled at m that contains an occurrence of t.
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 µ010 u1 µ. Let µ2 = µ01 µ00. Now let u2 be the rightmost transition with the same property 1 for the sequence µ2 and let µ2 = µ02 u2 µ00. The same argument as above yields 2 the sequence µ02 µ020 u2 u1µ. Exhaustive repetition of this procedure yields smaller and smaller sequences µi to be considered and eventually the sequence µ0k µ0k0 uk uk i . . . u1 µ such that no further transition to be postponed can be found in µ0k µ0k0. So this sequence is minimal towards t. By construction, it is a subsequence of , and uk uk i . . . u1 µ is the complementary subsequence. tu
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.
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 µ010 and µ2 = µ02 u µ00. When this claim is proven, we know by conflict-freeness that 2 there are also initially enabled occurrence sequences u µ01 µ010 and u µ02 µ00. By the 2 induction hypothesis applied to the (new initial) marking obtained by firing u and to the sequences µ01 µ010 and µ02 µ020, 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 µ00, now such that no transition of µ02 occurs in 2 µ1 and the first transition in µ00, say v, occurs in µ1. By assumption, v is not 2 initially enabled. The sequence µ020 is not empty because both µ1 and µ2 contain t. We divide µ1 as µ01 µ010 such that µ010 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 µ0 . By conflict-freeness and since the sets of 2 occurring transitions in µ01 and µ02 are disjoint, we can also fire both, i.e. µ01 µ0 , 2 from the initial marking. This yields a marking with two tokens on the place s, contradicting 1-boundedness. tu
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 controllable 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 response 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 containing 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 controllable 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 above considerations, this way defining ' t on the fly, until we eventually force t to occur.
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., observable 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 conflicts 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 = v1v2 . . . 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 preset, 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 conflictfree. 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 µ satisfying µ = µ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. 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., µ0 0 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 considering 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 1u1 2 where 2 is again ' t-maximal, and 2 is shorter than . By the induction hypothesis, 2 contains t, and therefore so does . tu
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.
The net shown in Fig. 4.c is conflict-free w.r.t. all its uncontrollable transitions. 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
Petri nets are widely used in software engineering for modeling and verifying
software systems [
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 [
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
that the net behaves weakly fair. A similar notion, T -liveness, yet for different
motivations, is represented in [
In general, liveness does not imply observable liveness and neither the opposite 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 transition 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 transitions 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
uncontrolled 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
behavior, which preserves observable liveness. Reduction rules, as defined e.g. in
[
As a future work, we plan to consider an automata approach for the implementation 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 automata 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 [
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
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 [
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 Applicativi’, code H41J12000190001.