9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Computation Tree Logic with Deadlock Detection (extended abstract)

Computation Tree Logic with Deadlock Detection

(extended abstract) Rob van Glabbeek 1,2 , Bas Luttik 3,4 & Nikola Trˇka 3 c

2 3

National ICT Australia, Sydney, Australia School of Computer Science and Engineering, Univ. of New South Wales, Sydney Dept. of Math. & Comp. Sc., Technische Universiteit Eindhoven, The Netherlands 4 CWI, The Netherlands

1

Abstract. We study the equivalence relation on states of labelled transition systems of satisfying the same formulas in Computation Tree Logic without the next state modality (CTL?X ). This relation is obtained by De Nicola & Vaandrager by translating labelled transition systems to Kripke structures, while lifting the totality restriction on the latter. They characterised it as divergence sensitive branching bisimulation equivalence. We ?nd that this equivalence fails to be a congruence for interleaving parallel composition. The reason is that the proposed application of CTL?X to non-total Kripke structures lacks the expressiveness to cope with deadlock properties that are important in the context of parallel composition. We propose an extension of CTL?X , or an alternative treatment of nontotality, that ?lls this hiatus. The equivalence induced by our extension is characterised as branching bisimulation equivalence with explicit divergence, which is, moreover, shown to be the coarsest congruence contained in divergence sensitive branching bisimulation equivalence.

1

Introduction

CTL? [4] is a powerful temporal logic combining linear time and branching time modalities; it generalises the branching time temporal logic CTL [3]. CTL? is interpreted in terms of Kripke structures. As the next state modality X is incompatible with abstraction of the notion of state, it is often excluded in high-level speci?cations. By CTL? we denote CTL? without this modality. To characterise ?X the equivalence induced on states of Kripke structures by validity of CTL? for?X mulas, Browne, Clarke & Gr¨ mberg [1] de?ned the notion of stuttering equivu alence. They proved that two states in a ?nite Kripke structure are stuttering equivalent if and only if they satisfy the same CTL? formulas, and moreover, ?X they established that this is already the case if and only if the two states satisfy the same CTL?X formulas. There is an intuitive correspondence between the notions of stuttering equivalence on Kripke structures and branching bisimulation equivalence on labelled transition systems (LTSs) as de?ned in [8]. De Nicola & Vaandrager [2] have provided a framework for constructing natural translations between LTSs and

2

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

Kripke structures in which this correspondence can be formalised. Stuttering equivalence corresponds in their framework to a divergence sensitive variant of branching bisimulation equivalence, and conversely, branching bisimulation equivalence corresponds to a divergence blind variant of stuttering equivalence. The latter characterises the equivalence induced on states of Kripke structures by a divergence blind variant of validity of CTL? formulas. ?X In [3, 4, 1] and other work on CTL? , Kripke structures are required to be total, meaning that every state has an outgoing transition. These correspond with LTSs that are deadlock-free. In the world of LTSs requiring deadlock-freeness is considered a serious limitation, as deadlock is introduced by useful process algebraic operators like the restriction of CCS and the synchronous parallel composition of CSP. Conceptually, a deadlock may arise as the result of an unsuccessful synchronisation attempt between parallel components, and often one wants to verify that the result of a parallel composition is deadlock-free. This is possible only when working in a model of concurrency where deadlocks can be expressed. Through the translations of [2] it is possible to de?ne the validity of CTL? ?X formulas on states of LTSs. To apply CTL? -formulas to LTSs that may contain ?X deadlocks we consider Kripke structures with deadlocks as well, and hence lift the requirement of totality. Following [2], we do so by using maximal paths instead of in?nite paths in the de?nition of validity of CTL? formulas. Barring further ?X changes, this amounts to the addition of a self loop to every deadlock state. As a consequence, CTL? formulas cannot see the di?erence between a state ?X without outgoing transitions (a deadlock ) and one whose only outgoing transition constitutes a self loop (a livelock ), and accordingly a deadlock state is stuttering equivalent to a livelock state that satis?es the same atomic propositions. This paper will challenge the wisdom of this set-up. We observe that for systems with deadlock, the divergence sensitive branching bisimulation equivalence of [2] fails to be a congruence for interleaving operators. We characterise the coarsest congruence contained in divergence sensitive branching bisimulation equivalence as the branching bisimulation equivalence with explicit divergence, introduced in [8]. This equivalence di?ers from divergence sensitive branching bisimulation equivalence in that it distinguishes deadlock and livelock. For deadlock-free systems the equivalences coincide. That divergence sensitive branching bisimulation equivalence is not a congruence for interleaving operators means that there are properties of concurrent systems, pertaining to their deadlock behaviour, that cannot be expressed in CTL? , but that can be expressed in terms of the validity of a CTL? formula ?X ?X on the result of putting these systems in a given context involving an interleaving operator. We ?nd this unsatisfactory, and therefore propose an extension of CTL? in which this type of property can be expressed directly. We obtain that ?X two states are branching bisimulation equivalent with explicit divergence if and only if they satisfy the same formulas in the resulting logic. Treating CTL?X in the same way leads either to an extension of CTL?X or, equivalently, to a modi?cation of its semantics. The new semantics we propose for CTL?X is a valid extension of the original semantics [3] to non-total Kripke

Computation Tree Logic with Deadlock Detection

3

structures. It slightly di?ers from the semantics of [2] and it is arguably better suited to deal with deadlock behaviour. Instead of extending CTL? or modifying CTL?X we also achieve the same ?X e?ect by amending the translation from LTSs to Kripke structures in such a way that every LTS maps to a total Kripke structure. In this extended abstract most proofs are omitted. They can be found in the full version of this paper [7].

2

CTL? and stuttering equivalence ?X

We presuppose a set AP of atomic propositions. A Kripke structure is a tuple (S, L, →) consisting of a set of states S, a labelling function L : S → 2AP and a transition relation → ? S × S. For the remainder of the section we ?x a Kripke structure (S, L, →). A ?nite path from s is a ?nite sequence of states s0 , . . . , sn such that s = s0 and sk ?→ sk+1 for all 0 ≤ k < n. An in?nite path from s is an in?nite sequence ? of states s0 , s1 , s2 , . . . such that s = s0 and sk ?→ sk+1 for all k ∈ ω. A path ? is a ?nite or in?nite path. A maximal path is an in?nite path or a ?nite path s0 , . . . , sn such that ??s′ . s n ?→ s′ . We write π ¤ π ′ if the path π ′ is a su?x of ? the path π, and π ? π ′ if π ¤ π ′ and π = π ′ . Temporal properties of states in S are de?ned using CTL? formulas. ?X De?nition 1. The classes Φ of CTL? state formulas and Ψ of CTL? path ?X ?X formulas are generated by the following grammar: ? ::= p | ?? | Φ′ | ?ψ ψ ::= ? | ?ψ | Ψ′ | ψ U ψ

with p ∈ AP, ? ∈ Φ, Φ′ ? Φ, ψ ∈ Ψ and Ψ ′ ? Ψ . In case the cardinality of the set of states of our Kripke structure is less than some in?nite cardinal κ, we may require that |Φ′ | < κ and |Ψ ′ | < κ in conjunctions, thus obtaining a set of formulas rather than a proper class. Normally, S is required to be ?nite, and accordingly CTL? admits ?nite conjunctions only. ?X De?nition 2. We de?ne when a CTL? state formula ? is valid in a state s ?X (notation: s |= ?) and when a CTL? path formula ψ is valid on a maximal ?X path π (notation: π |= ψ) by simultaneous induction as follows: ? ? ? ? ? ? ? ? s |= p i? p ∈ L(s); s |= ?? i? s |= ?; s |= Φ′ i? s |= ? for all ? ∈ Φ′ ; s |= ?ψ i? there exists a maximal path π from s such that π |= ψ; π |= ? i? s is the ?rst state of π and s |= ?; π |= ?ψ i? π |= ψ; π |= Ψ ′ i? π |= ψ for all ψ ∈ Ψ ′ ; and π |= ψ U ψ ′ i? there exists a su?x π ′ of π such that π ′ |= ψ ′ , and π ′′ |= ψ for all π ¤ π ′′ ? π ′ .

4

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

A formula ψ U ψ ′ says that, along a given path, ψ holds until ψ ′ holds. One writes ? for the empty conjunction (which is always valid), Fψ for ? U ψ (“ψ will hold eventually”) and Gψ for ?F?ψ (“ψ holds always (along a path)”). The above is the standard, divergence sensitive interpretation of CTL? [4, 1], ?X but extended to Kripke structures that are not required to be total. Following [2], this is achieved by using maximal paths in the de?nition of validity of CTL? ?X formulas, instead of the traditional use of in?nite paths [4, 1]. The resulting de?nition generalises the traditional one, because for total Kripke structures a path is maximal i? it is in?nite. An equivalent way of thinking of this generalisation of CTL? to non-total ?X Kripke structures is by means of a transformation that makes a Kripke structure K total by the addition of a self loop s ?→ s to every deadlock state s, together ? with the convention that a formula is valid in a state of K i? it is valid in the same state of the total Kripke structure obtained by this transformation. It is not hard to check that this yields the same notion of validity as our De?nition 2. The divergence blind interpretation of [2] (notation: s |=db ? and π |=db ψ) is obtained by dropping the word “maximal” in the fourth clause of De?nition 2. De?nition 3. A colouring is a function C : S → C, for C any set of colours. Given a colouring C and a (?nite or in?nite) path π = s0 , s1 , s2 , . . . from s, let C(π) be the sequence of colours obtained from C(s0 ), C(s1 ), C(s2 ), . . . by contracting all (?nite or in?nite) subsequences C, C, C, . . . to C. The sequence C(π) is called a C-coloured trace of s; it is complete if π is maximal. A colouring C is [fully] consistent if two states of the same colour always satisfy the same atomic propositions and have the same [complete] C-coloured traces. Two states s and t are divergence blind stuttering equivalent, notation s ≈dbs t, if there exists a consistent colouring C such that C(s) = C(t). They are (divergence sensitive) stuttering equivalent, notation s ≈s t, if there exists a fully consistent colouring C such that C(s) = C(t). Lemma 1. Let C be a colouring such that two states with the same colour have the same C-coloured traces of length two. Then C is consistent. Lemma 2. Let C be a colouring such that two states with the same colour have the same C-coloured traces of length two, and the same complete C-coloured traces of length one. Then C is fully consistent. The following two theorems were proved in [2] and [1], respectively, for states s and t in a ?nite Kripke structure. Here we drop the ?niteness restriction. Theorem 1. s ≈dbs t i? s |=db ? ? t |=db ? for all CTL? state formulas ?. ?X Theorem 2. s ≈s t i? s |= ? ? t |= ? for all CTL? state formulas ?. ?X Corollary 1. ≈dbs and ≈s are equivalence relations.

Computation Tree Logic with Deadlock Detection

5

Note that, for any colouring C, the C-coloured traces of a state s are completely determined by the complete C-coloured traces of s, namely as their pre?xes. Hence, any colouring that is fully consistent is certainly consistent, and thus ≈s is a ?ner (i.e. smaller, more discriminating) equivalence relation than ≈dbs . Above, the divergence blind interpretation of CTL? is de?ned by using paths ?X instead of maximal paths. It can equivalently be de?ned in terms of a transformation on Kripke structures, namely the addition of a self loop s ?→ s for every ? state s. Now s ≈dbs t holds in a certain Kripke structure i? s ≈s t holds in the Kripke structure obtained by adding all these self loops. This is because the colour of a path doesn’t change when self-loops are added to it, and up to self loops any path is maximal. Likewise, s |=db ? in the original Kripke structure i? s |= ? in the modi?ed one. Just like ≈dbs can be expressed in terms of ≈s by means of a transformation on Kripke structures, by means of a di?erent transformation, at least for ?nite Kripke structures, ≈s can be expressed in terms of ≈dbs . This is done in [2], De?nitions 3.2.6 and 3.2.7.

3

Branching bisimulation in terms of coloured traces

We presuppose a set A of actions with a special element τ ∈ A. A labelled transition system (LTS) is a structure (S, →) consisting of a set of states S and a transition relation → ? S × A × S. For the remainder of the section we ?x a a labelled transition system (S, →). We write s ?→ s′ for (s, a, s′ ) ∈ →. ? A path from s is an alternating sequence s0 , a1 , s1 , a2 , s2 , . . . of states and actions, ending with a state if the sequence is ?nite, such that s = s0 and ak sk?1 ? → sk for all relevant k > 0. A maximal path is an in?nite path or a ?nite ? a ? path s0 , a1 , s1 , a2 , . . . , an , sn such that ??a, s′ . s n ?→ s′ . We write π ¤ π ′ if the path π ′ is a su?x of the path π, and π ? π ′ if π ¤ π ′ and π = π ′ . De?nition 4. A colouring is a function C : S → C, for C any set of colours. For π = s0 , a1 , s1 , a2 , s2 , . . . a path from s, let C(π) be the alternating sequence of colours and actions obtained from C(s0 ), a1 , C(s1 ), a2 , C(s2 ), . . . by contracting all (?nite or in?nite) subsequences C, τ, C, τ, C, . . . to C. The sequence C(π) is called a C-coloured trace of s; it is complete if π is maximal; it is divergent if it is ?nite whilst π is in?nite. A colouring C is [fully] consistent if two states of the same colour always have the same [complete] C-coloured traces. Two states s and t are (divergence blind) branching bisimulation equivalent, notation s ?b t, if there exists a consistent colouring C such that C(s) = C(t). They are divergence sensitive branching bisimulation equivalent, notation s ?λ t, if there exists a fully consistent colouring C b such that C(s) = C(t). A consistent colouring preserves divergence if two states of the same colour always have the same divergent C-coloured traces. Two states s and t are branching bisimulation equivalent with explicit divergence, notation s ?? t, if there exists b a consistent, divergence preserving colouring C with C(s) = C(t).

6

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

In the de?nition of ?? above, consistency and preservation of divergence appear b as two separate properties of colourings. Instead we could have integrated them by adding an extra bit (?) at the end of those ?nite coloured traces that stem from in?nite paths. Likewise, ?λ could have been de?ned by adding such an b extra bit at the end of those ?nite coloured traces that stem from maximal paths. Lemmas 1 and 2 about colourings on Kripke structures apply to labelled transition systems as well. Lemma 3. Let C be a colouring such that two states with the same colour have the same C-coloured traces of length three (i.e. colour - action - colour). Then C is consistent. Lemma 4. Let C be a consistent colouring such that two states with the same colour have the same complete C-coloured traces of length one. Then C is fully consistent. Lemma 5. Let C be a consistent colouring such that two states with the same colour have the same divergent C-coloured traces of length one. Then C preserves divergence. Branching bisimulation equivalence and branching bisimulation equivalence with explicit divergence were originally de?ned in Van Glabbeek & Weijland [8]. There, only ?nite coloured traces are considered, and a consistent colouring was de?ned as a colouring with the property that two states have the same colour only if they have the same ?nite coloured traces. By Lemma 3 this yields the same concept of consistent colouring as De?nition 4 above. In [8], a consistent colouring is said to preserve divergence if no divergent state has the same colour as a nondivergent state. Here a state s is divergent if it is the starting point of an in?nite path of which all nodes have the same colour. This is the case if s has a divergent coloured trace of length one. Now Lemma 5 says that the de?nition of preservation of divergence from [8] agrees with the one proposed above. Hence the concepts of branching bisimulation and branching bisimulation with explicit divergence of [8] agree with ours. Theorem 3. ?b , ?λ and ?? are equivalence relations. b b Proof. We show the proof for ?b ; the other two cases proceed likewise. We will regard any equivalence relation on S as a colouring, the colour of a state being its equivalence class. Conversely, any colouring can be considered as an equivalence relation on states. The diagonal on S (i.e., the binary relation {(s, s) | s ∈ S}) is a consistent colouring, so ?b is re?exive. That ?b is symmetric is immediate from the required symmetry of colourings. To prove that ?b is transitive, suppose s ?b t and t ?b u. So there exist consistent colourings C and D with C(s) = C(t) and D(t) = D(u). Let E be the ?nest equivalence relation containing C and D. Then E(s) = E(t) = E(u). It su?ces to show that E is consistent.

Computation Tree Logic with Deadlock Detection

7

First of all note that the E-colour of a state is completely determined by its C-colour, as well as by its D-colour: C(p) = C(q) ? E(p) = E(q) and D(p) = D(q) ? E(p) = E(q) for all p, q ∈ S. Thus, if two states have the same sets of C-coloured traces or the same sets of D-coloured traces, they must also have the same sets of E-coloured traces. Suppose E(p) = E(q). Then there must be a sequence of states (pi )0≤i≤n such that p = p0 , q = pn and for 0 ≤ i < n we have either C(pi ) = C(pi+1 ) or D(pi ) = D(pi+1 ). As C and D are consistent colourings, pi and pi+1 have the same C-coloured traces or the same D-coloured traces. In either case they also have the same E-coloured traces. This holds for 0 ≤ i < n, so p and q have the same E-coloured traces. Thus E is consistent. P Lemma 6. Let C be a consistent colouring and s ∈ S. Then the complete Ccoloured traces of s consist of the C-coloured traces of s that are in?nite, divergent, or maximal, in the sense that they cannot be extended. As for Kripke structures, for any colouring C, the C-coloured traces of a state s are the pre?xes of the complete C-coloured traces of s. Moreover, Lemma 6 says that the complete C-coloured traces of a state s are completely determined by the C-coloured traces of s together with the divergent C-coloured traces of s. Hence, any colouring that is consistent and preserves divergence is also fully consistent. Therefore, ?? is ?ner than ?λ , which is ?ner than ?b . b b The di?erence between ?λ and ?? is that only the latter sees the di?erence b b between those maximal ?nite coloured traces that stem from ?nite paths (ending in deadlock ) and those that stem from in?nite paths (ending in livelock ). For deadlock-free LTSs (having no states s with ??a, s′ . s ?a s′ ) the equivalences ? → ?λ and ?? coincide. b b

4

Translating between Kripke structures and labelled transition systems

We presuppose a set A of actions with a special element τ ∈ A, and a set AP of atomic propositions. A doubly labelled transition system (L2 TS) is a structure (S, L, →) that consists of a set of states S, a labelling function L : S → 2AP and a labelled transition relation → ? S × A × S. From an L2 TS one naturally obtains an LTS by omitting the labelling function L, and a Kripke structure by replacing the labelled transition relation by one from which the labels are omitted. We call these the LTS or Kripke structure associated to the L2 TS. An L2 TS (S, L, →) is consistent if it satis?es the following three conditions: (i) if s ?→ t, then (L(s) = L(t) i? a = τ ); ? a (ii) if s ?→ t, s′ ?a′ t ′ and L(s) = L(s′ ), then L(t) = L(t′ ); and ? ? → a a (iii) if s ?→ t, s′ ?→ t ′ , L(s) = L(s′ ) and L(t) = L(t′ ), then a = a′ . ? ? Consistent L2 TSs were introduced in De Nicola & Vaandrager [2] for studying relationships between notions de?ned for Kripke structures and notions de?ned

a

8

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

for LTSs. Condition (iii) says that the label of a transition is fully determined by the labels of its source and target state, whereas condition (ii) entails that the label of a state t reachable from a state s is completely determined by the label of s and the sequence of labels of the transitions leading from s to t. Many semantic equivalences on LTSs, such as ?b , ?λ and ?? , are considb b ered in the literature; for an overview see [5]. De?nition 5. Any semantic equivalence ? on LTSs extends to L2 TSs by declaring, for all states s and t in an L2 TS, that s ? t i? L(s) = L(t) and s ? t in the associated LTS. Any semantic equivalence ? on Kripke structures extends to L2 TSs by declaring, for all states s and t in an L2 TS, that s ? t i? s ? t in the associated Kripke structure. The following theorem was proved in [2] for ?nite consistent L2 TSs. Here we drop the ?niteness restriction. Theorem 4. On a consistent L2TS, ≈dbs equals ?b , and ≈s equals ?λ . b Observation 1. For every Kripke structure K there exists a consistent L2TS D such that K is the Kripke structure associated to D. One way to obtain D is to label any transition s ?→ t by the pair (L(s), L(t)) ? (or simply by L(t)) when L(s) = L(t), or τ when L(s) = L(t). An alternative is the label (L(s) ? L(t), L(t) ? L(s)), where (?, ?) is identi?ed with τ . Unlike the situation for Kripke structures (Observation 1) it is not the case that every LTS can be obtained as the LTS associated to a consistent L2 TS. A simple counterexample is presented in [2]. Thus, in encoding LTSs as L2 TSs, it is in general not possible to keep the set of states the same. De?nition 6. An LTS-to-L2TS transformation η consist of a function taking any LTS L to a consistent L2 TS η(L), and in addition taking any state s in L to a state η(s) in η(L). Such a transformation should at least satisfy s ?λ t ? b η(s) ?λ η(t), that is, it preserves (“?”) and re?ects (“?”) divergence sensitive b branching bisimulation equivalence, and likewise for ?b , and ?? . b A popular LTS-to-L2 TS transformation is presented in [2]. It takes an LTS L = (S, →) to an L2 TS η(L) by inserting a new state halfway any transition s ?a t ? → with a = τ . This new state is labelled {a}, and each of the two transitions a replacing s ?→ t (from s to the new state and from there to t) is labelled a. ? Transitions s ?τ t are untouched. One takes η(s) = s for s ∈ S and all such ? → states from L are labelled {⊥} in η(L). (Consult [2] for the formal de?nition and examples.) In [2] it is shown that this transformation preserves and re?ects ?λ ; b the same proof applies to ?b and ?? . b An LTS-to-L2 TS transformation η yields an LTS-to-Kripke-structure transformation that we also call η, namely the one transforming an LTS L into the Kripke structure associated to η(L). In fact, using Theorem 4 and Observation 1, any LTS-to-Kripke-structure transformation η that preserves and re?ects the required equivalences can be obtained in this way.

Computation Tree Logic with Deadlock Detection

9

An LTS-to-L2 TS transformation η makes it possible to de?ne when a state s η in an LTS satis?es a CTL? formula ?. Namely, one de?nes s |= ? i? η(s) |= ?. ? This way, CTL can be used as temporal logic on LTSs. Theorem 5. Let s and t be states in an LTS, and let η be an LTS-to-L2TS transformation. Then s ?b t i? s |=η ? ? t |=η ? for all CTL? state formulas ? ?X db db s ?λ t i? s |=η ? ? t |=η ? for all CTL? state formulas ?. ?X b Proof. This is an immediate consequence of the requirement that η preserves and re?ects ?b and ?λ , in combination with Theorems 1, 2 and 4. P b

5

Parallel composition

For a behavioural equivalence to be useful in a process algebraic setting, it is essential that it is a congruence for the operations under consideration. In this section we prove that ?? and ?b are congruences for the merge or interleavb ing operator . This operator is often used to represent (asynchronous) parallel composition. However, ?λ fails to be a congruence for . We characterise the b least discriminating congruence that makes all the distinctions of ?λ as ?? . b b De?nition 7. A binary operation on the states of an LTS is a merge if for all a s, t, u ∈ S and for all a ∈ A it holds that s t ?→ u i? ? ? there exists s′ ∈ S such that s ?→ s′ and u = s′ t; or ? a ? there exists t′ ∈ S such that t ?→ t′ and u = s t′ . ? Henceforth we deal with LTSs with a merge . Theorem 6. The relation ?? is a congruence for , i.e., if s ?? t and u ?? v, b b b then s u ?? t v. b Proof. Let R be the re?exive and transitive closure of the relation {(p q, p′ q ′ ) | p ?? p′ & q ?? q ′ } . b b Let C be the function that assigns to each state its equivalence class with respect to R. It su?ces to prove that C is a consistent divergence preserving colouring. So suppose C(r) = C(r′ ). Using Lemmas 3 and 5 it su?ces to show that r and r′ have the same C-coloured traces of length three and the same divergent Ccoloured traces of length one. It is straightforward, but notationally cumbersome, to establish this in the special case that r = p q and r′ = p′ q ′ with p ?? p′ b and q ?? q ′ . The general case then follows by induction on the length of a chain b of pairs from the relation displayed above showing that the pair (r, r′ ) is in its re?exive and transitive closure. P A similar proof shows that also ?b is a congruence for . However, ?λ is not. b

a

10

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

Example 1. Let 0 be a state (in an LTS) without outgoing transitions, and let ?0 be a state with a τ -loop (an outgoing τ -labelled transition to itself) and no a other outgoing transitions. Let a be a state with a ?→ 0 and no other outgoing ? λ λ transitions. Then 0 ?b ?0 but 0 a ?b ?0 a. The reason is that ?0 a has a maximal path that stays in its initial state, whereas 0 a has not. This problem does not apply to ?b because 0 a ?b ?0 a. It does not apply to ?? because b 0 ?? ?0. b The example above involves a deadlock state, namely 0. This is unavoidable, as on LTSs without deadlock ?λ coincides with ?? (cf. Section 3) and hence is a b b congruence for . The standard solution to the problem of an equivalence ? failing to be a congruence for a desirable operator Op is to replace it by the coarsest congruence for Op that is included in ? [9]. Applying this technique to the current situation, the coarsest congruence for included in ?λ turns out to be ?? . b b Theorem 7. ?? is the coarsest congruence for b that is included in ?λ .1 b

Proof. We have already seen that ?? is a congruence for , and that it is b included in ?λ . To show that it is the coarsest, it su?ces to show that whenever b s ?? t, we can ?nd a state u such that s u ?λ t u. In fact, we can always b b take u to be the state a from Example 1, for a an action that does not occur in any path from s or t. Namely, suppose that s a ?λ t a. Let C be a fully consistent colouring b with C(s a) = C(t a). De?ne the colouring D by D(p) = C(p a) for p a state reachable from s or t, and D(p) = p otherwise. Then D(s) = D(t). It su?ces to show that D is consistent and preserves divergence, implying s ?? t. b So suppose D(p) = D(q) with p = q. Then C(p a) = C(q a). First we show that p and q have the same D-coloured traces. Let σ be a D-coloured trace of p. Then σ is also a C-coloured trace of p a. As p a and q a have the same complete C-coloured traces, they surely have the same C-coloured traces (for the coloured traces of a state are the pre?xes of its complete coloured traces). Hence σ is a C-coloured trace of q a. As p is reachable from s or t, the action a cannot occur in σ. Therefore, σ must also be a D-coloured trace of q. By symmetry, any D-coloured trace of q is also a D-coloured trace of p, and hence p and q have the same D-coloured traces. Next, we show that p and q have the same divergent D-coloured traces. So let σ be a divergent D-coloured trace of p. Then σ is also a divergent C-coloured

1

Strictly speaking, we merely show that ?? is the coarsest congruence for that b is included in ?λ and satis?es the Fresh Atom Principle (FAP). This principle, b described in [6], is satis?ed by a semantic equivalence ? on LTSs when ? on an LTS L can always be obtained as the restriction of ? on any given larger LTS of which L is a subLTS, and whose transition labels may be drawn from a larger set of actions than those of L. FAP allows us to use the state a that ?gures in the proof of Theorem 7, regardless of whether such a state, or the fresh action a, occurs in the given LTS or not. FAP is satis?ed by virtually all semantic equivalences documented in the literature, and can be used as a sanity check for meaningful equivalences [6].

Computation Tree Logic with Deadlock Detection

11

trace of p a. Hence σ is a complete C-coloured trace of p a and thus also of q a. As the action a cannot occur in σ, it is not possible that σ stems from a ?nite maximal path from q a. Therefore, σ must be a divergent C-coloured trace of q a, and hence a divergent D-coloured trace of q. Again invoking symmetry, p and q have the same divergent D-coloured traces. P It follows that D is consistent and preserves divergence; thus s ?? t. b So if one is in search of a semantics such that, for s and t states in an LTS, η η ? if there is a CTL? state formula ? such that s |= ? but t |= ?, then s ?X and t should be distinguished, ? if s and t can be distinguished after placing them in a context u for some u, then they should be distinguished to start with ? and no two states should be distinguished unless this is required by the previous two conditions, then branching bisimulation semantics with explicit divergence is the answer, η η for s ?? t i? for all u and all ? ∈ Φ we have s u |= ? ? t u |= ?. b

6

Adding deadlock detection to CTL? ?X

We saw above that there are important properties of states s in an LTS that can be expressed in terms of a context u and a CTL? formula ?, namely ?X η as s u |= ?, but that cannot be directly expressed in terms of CTL? . This ?X is somewhat unsatisfactory, and therefore we propose an extension of CTL? in ?X which this type of property can be expressed directly. We add a path modality ∞ that is valid on a path π i? π is in?nite. De?nition 8. The syntax of CTL? is given by ? ? ::= p | ?? | Φ′ | ?ψ ψ ::= ? | ?ψ | Ψ′ | ψ U ψ | ∞

with p ∈ AP, ? ∈ Φ, Φ′ ? Φ, ψ ∈ Ψ and Ψ ′ ? Ψ . Validity is de?ned as in De?nition 2, but adding the clause ? π |= ∞ i? the path π is in?nite. We write ?∞ ψ for ?(∞ ∧ ψ); this formula holds in a state s if there exists an in?nite path π from s such that π |= ψ. Likewise ?∞ ψ = ?(∞ → ψ) holds in s if for all in?nite paths π from s we have that s |= ψ. These constructs are dual, in the sense that s |= ??∞ ψ i? s |= ?∞ ?ψ. The negation of ∞ holds for a maximal path π i? π is ?nite, and hence ends in a deadlock. It is tempting to simply extend CTL? with a state formula δ ?X such that s |= δ i? ??s′ . s ?→ s′ . This would make it possible to express ∞ ? as ?Fδ. However, this would make the resulting logic too expressive: the two states in the Kripke structure ? ?→ ? (with the empty labelling) are branching ? bisimulation equivalent with explicit divergence, yet they would be distinguished by this extension of CTL? , as only the last state satis?es δ. ?X

12

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

CTL? is an extension of CTL? . There is no need for a similar extension of ? ?X CTL? , for δ can be expressed as ??X?. The de?nition of branching bisimulation equivalence with explicit divergence lifts easily to Kripke structures: s ?? t, for s and t states in a Kripke structure, b i? there exists a consistent and divergence preserving colouring C such that C(s) = C(t). Here divergence preserving is de?ned as in Section 3; by Lemma 5, this time applied to Kripke structures, a colouring preserves divergence i?, for any states s and t, C(s) = C(t) implies for any in?nite path π from s with C(π) = C(s) there is an in?nite path ρ from t with C(ρ) = C(t). Theorem 8. s ?? t i? s |= ? ? t |= ? for all CTL? state formulas ?. ? b

7

Adding deadlock detection to CTL?X

CTL?X is the sublogic of CTL? that only allows path formulas of the form ?X ? U ? ′ and ?(? U ? ′ ), where ? and ? ′ are state formulas. Equivalently, it can be de?ned as only allowing path formulas of the form ? U ? ′ and G?, for we have s |= ?G? i? s |= ??(? U ??) s |= ??(? U ? ′ ) i? s |= ?[(?? ′ ) U ?(? ∨ ? ′ )] ∨ ?G?? ′ . Theorems 1 and 2 are also valid when using CTL?X instead of CTL? . ?X A natural proposal for CTL? would be to add the path quanti?er ?∞ to CTL?X , thus yielding the syntax ? ::= p | ?? | Φ′ | ?(? U ?) | ?∞ (? U ?) | ?G? | ?∞ G? .

However, we can economise on that, for s |= ?∞ (? U ? ′ ) i? s |= ?(? U (? ′ ∧ ?∞ G?)) s |= ?G? i? s |= ?∞ G? ∨ ?(? U (?G?)) where ?G? is an abbreviation for ??(? U ??). Hence CTL? can be given by the syntax ? ::= p | ?? | Φ′ | ?(? U ?) | ?∞ G? . This language is su?ciently expressive to characterise branching bisimulation equivalence with explicit divergence: Theorem 9. s ?? t i? s |= ? ? t |= ? for all CTL? formulas ?. b It is tempting to simply write ?∞ G as ?G; that is, to keep the same syntax as for CTL?X but de?ne its semantics in such a way that ?(? U ? ′ ) asks merely for a ?nite path, whereas ?G? asks for an in?nite one. This deadlock sensitive interpretation of CTL?X is an alternative for the interpretation of [2]. It is consistent with the classical interpretation of CTL [4, 1], as for total Kripke structures there is no di?erence between ?∞ and ?.

Computation Tree Logic with Deadlock Detection

13

8

The deadlock extension of Kripke structures

Following De Nicola & Vaandrager [2] we have applied CTL? to non-total ?X Kripke structures by using maximal instead of in?nite paths in the de?nition of validity. As remarked in Section 2, the same e?ect can be obtained by transforming a non-total Kripke structure into a total one by adding a self loop s?→s ? to every deadlock state s, and applying the standard CTL? semantics to the ?X resulting total Kripke structure. However, the latter does not apply to CTL? , ? because the self loop s ?→ s invalidates the formula ??∞ that holds in any ? deadlock state s. Here we de?ne another transformation on Kripke structures that makes any Kripke structure total, and allows encoding of CTL? in terms ? of CTL? . ?X De?nition 9. The deadlock extension D(K) of a Kripke structure K is obtained by the addition of a fresh state sδ , labelled by the fresh atomic proposition δ, together with a transition from sδ and from every deadlock state in K to sδ . Theorem 10. Let K be a Kripke structure, with states s and t. Then s ?? t b within the Kripke structure K i? s ?? t within the Kripke structure D(K). b Proof. “If”: Let D be a consistent and divergence preserving colouring on D(K). Note that D(sδ ) = D(s) for any state s = sδ in D(K). Let C be the restriction of D to the states of K. Then the C-coloured traces of a state s in K equal the Dcoloured traces of s in D(K), but with the colour D(sδ ) omitted from the end of such traces. It follows that C is consistent. It preserves divergence by Lemma 5. “Only if”: Let C be a consistent and divergence preserving colouring on K. Extend it to a colouring D on D(K) by assigning a fresh colour δ to the extra state sδ of D(K). It su?ces to check that D is consistent and divergence preserving. Claim. From any state s in K with the same colour as a deadlock state t in K there must be a path π to a deadlock state such that C(π) = C(t). Proof of claim. As t has no C-coloured traces of length two, neither does s, and as t has no divergent C-coloured traces, neither does s. Thus, all paths from s are ?nite and only pass through states with colour C(t). Application of the claim. The D-coloured traces of length two of a state s = sδ in D(K) are the C-coloured traces of length two of the state s in K, together with the trace C(t)δ in case s has the same colour as a deadlock state t in K. Thus D is consistent by Lemma 1, and preserves divergence by Lemma 5. P The “if”-direction of the theorem, with a similar proof, also applies to ≈s and ≈dbs , but the “only if”-direction does not. As a counterexample, let K be a Kripke structure with a deadlock state d (having no outgoing transitions) and a livelock state l (with a self-loop as its only one outgoing transition); neither state satis?es any atomic propositions. In K we have d ≈s l, and hence d ≈dbs l, but in D(K) we have d ≈dbs l, and hence d ≈s l. Considering that Kripke structures of the form D(K) are total, and that on total Kripke structures ≈s and ?? coincide, it is in fact impossible to de?ne a b transformation like D for which Proposition 10 holds for both ?? and ≈s . b

14

Rob van Glabbeek, Bas Luttik & Nikola Trˇka c

Now let η be an arbitrary LTS-to-L2 TS-transformation, yielding an LTS-toKripke-structure transformation that is also called η (see Section 4). Then D ? η is not a valid LTS-to-Kripke-structure transformation as intended in [2], for it fails to preserve ?λ / ≈s and ?b / ≈dbs (cf. De?nition 6). Yet, it satis?es b s ?? t ? D ? η(s) ≈s D ? η(t) b (because s ?? t ? η(s) ?? η(t) ? D ? η(s) ?? D ? η(t) and on total Kripke b b b structures ?? and ≈s coincide), and as such it is a suitable transformation for b de?ning validity of CTL? formula on states in LTSs. We obtain: ?X Corollary 2. Let s and t be states in an LTS, and let η be an LTS-to-L2TS transformation. Then s ?? t i? s |=D?η ? ? t |=D?η ? for all CTL? state formulas ?. ?X b P

Thus, one way to make CTL? suitable for dealing with deadlock behaviour ?X on LTSs is to stick to total Kripke structures and translate LTSs to Kripke structures by a translation D ? η instead of a transformation η as proposed in [2]. This way branching bisimulation equivalence with explicit divergence becomes the natural counterpart of stuttering equivalence on Kripke structures, and we have the modal characterisation of Corollary 2. An alternative is to stick to more natural transformations η meeting the criteria on De?nition 6, apply the de?nition of validity of CTL? formulas to ?X non-total Kripke structures as in [2], and extend CTL? to CTL? as indicated ?X ? in Section 6. Below we show that these solutions lead to equally expressive logics on LTSs. De?nition 10. Given a set of atomic propositions, let CTL? be the logic CTL? ?X δ extended with an extra atomic proposition δ. The mappings D from CTL? to ? CTL? formula and E from CTL? to CTL? formula are de?ned inductively by δ ? δ D(p) D(??) D( i∈I ? i ) D(?ψ) D(?ψ) D( i∈I ψ i ) D(ψ U ψ ′ ) D(∞) Here δψ ′ = = = = = = = = = p ?δ ∧ ?D(?) i∈I D(? i ) ?D(ψ) ?δ ∧ ?D(ψ) i∈I D(ψ i ) D(ψ) U D(ψ ′ ) ?Fδ E (p) E(??) E( i∈I ? i ) E(?ψ) E(?ψ) E( i∈I ψ i ) E(ψ U ψ ′ ) E(δ) = = = = = = = = p ?E(?) i∈I E(? i ) ?E(ψ) ?E(ψ) i∈I E(ψ i ) (E(ψ) U δψ ′ ) ∨ (E(ψ) U E(ψ ′ )) ??

δ if sδ |= ?ψ ′ , and ψ U δ abbreviates ?∞ ∧ Gψ. ?? otherwise

Theorem 11. Let K be a Kripke structure and s a state in K. Then for any CTL? state formula ? we have s |= ? in K i? s |= D(?) in D(K), ? and for any CTL? state formula ? we have s |= ? in D(K) i? s |= E(?) in K. δ

Computation Tree Logic with Deadlock Detection

15

Proof. For a state formula ?, let [[?]]K denote the set of states s in K with s |= ?. Likewise, for a path formula ψ, [[ψ]]K denotes the set of maximal paths π in K with π |= ?. Note that there is a bijective correspondence between the maximal paths in K and those in D(K) not starting in sδ . A straightforward structural induction shows that [[?]]K = [[D(?)]]D(K) for any CTL? state formula ? and, ? up to the aforementioned bijective correspondence, [[ψ]]K = [[D(ψ)]]D(K) for any CTL? path formula ψ. ? For the second statement, let πδ be the unique path in D(K) starting in sδ . A straightforward structural induction shows that [[?]]D(K) ? {sδ } = [[E(?)]]K for any CTL? state formula ? and, up to the above bijective correspondence, δ [[ψ]]D(K) ? {πδ } = [[E(ψ)]]K for any CTL? path formula ψ. P δ In CTL? the path modality ∞ is equally expressive as the path modality ψ Uδ of ? De?nition 10, saying of a path that it is ?nite and all its su?xes satisfy ψ. This is because π |= ψ Uδ ? π |= ?∞∧Gψ and π |= ∞ ? π |= ?Fδ ? π |= ??Uδ. In this light, the encoding D of CTL? into CTL? merely adds a conjunct ?δ here ? δ and there. These conjuncts are not optional; they enable, for instance, the correct translation of the CTL? path formula Gp by the CTL? formula ?δ ∧ G(δ ∨ p). ? δ Theorem 12. Also the logics CTLδ and CTL? are equally expressive. Proof. This follows because D can be restricted to a mapping from CTL? to CTLδ formula and E to a mapping from CTL? to CTLδ formula. Details can be found in the full version of this paper [7].

References

1. M.C. Browne, E.M. Clarke & O. Gr¨mberg (1988): Characterizing ?nite Kripke u structures in propositional temporal logic. Theoretical Computer Science 59, pp. 115–131. 2. R. De Nicola & F.W. Vaandrager (1995): Three logics for branching bisimulation. Journal of the ACM 42(2), pp. 458–487. 3. E.A. Emerson & E.M. Clarke (1982): Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), pp. 241–266. 4. E.A. Emerson & J.Y. Halpern (1986): ‘Sometimes’ and ‘Not Never’ revisited: on branching time versus linear time temporal logic. Journal of the ACM 33(1), pp. 151–178. 5. R.J. van Glabbeek (1993): The linear time - branching time spectrum II. In E. Best, editor: Proceedings of CONCUR’93, LNCS 715, Springer, pp. 66–81. 6. R.J. van Glabbeek (2005): A characterisation of weak bisimulation congruence. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk & R. de Vrijer, editors: Processes, Terms and Cycles: Steps on the Road to In?nity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, LNCS 3838, Springer, pp. 26–39. 7. R.J. van Glabbeek, B. Luttik & N. Trˇka (2007): Computation Tree Logic with c Deadlock Detection. At http://theory.stanford.edu/~rvg/abstracts.html#73. 8. R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600. 9. R. Milner (1989): Communication and Concurrency. Prentice Hall, Englewood Cli?s.

- Computation Tree Logic with Deadlock Detection
- extended Computation Tree Logic
- On the logic and computation of Partial Equilibrium Models (extended abstract). Unpublished
- ABSTRACT Poster Abstract Cooperative Tracking with Binary-Detection Sensor Networks
- Rijke. Path constraints from a modal logic point of view (extended abstract
- TTree Tree-based state generalization with temporally abstract actions
- Logic programming with bunched implications (extended abstract
- Abstract 1 Making Large Class Teaching More Adaptive With the Logic-ITA
- Axiomatising extended computation tree logic, in trees in algebra and programming
- Distributed Deduction a Linear Logic View of Parallel Computation (Extended Abstract)
- 学霸百科
- 新词新语