4.4 General Temporal properties
4.4.1 A Linear Time Logic
The modal µ-calculus is classified as a branching time logic referring to the property that the modalitiesa and [a] quantify over possible futures. Nev-ertheless, expressivity results show that alsolinear time logics referring in a certain sense to only one possible future, can be embedded into the modal µ-calculus ([49, 79, 30]). We will consider a very succinct embedding of a simple logic combining linear and branching time features, which apart from the usefulness of the translation will supply us with a collection of derived operators (or ‘macros’).
4.4 General Temporal properties 97 The logic will be a sub-logic of the logic CTL∗(Computation Tree Logic) [36]. We first, however, describe CTL∗ in a slightly weaker version by omit-ting the ‘until’-operatorU, instead having explicit versions of the ‘eventually’-and ‘always’-operators ✸ and ✷. The syntax of this mini-CTL∗ is given by the grammar:
Φ ::=p|Φ∨Φ|Φ∧Φ| Φ| Φ|✷Φ|✸Φ| ∃Φ| ∀Φ
where p is are a propositional constant, a ‘next’-operator, a ‘weak next’-operator and ∃and ∀are path quantifiers. We use greek capital letters Φ,Θ, . . . to range over linear time formulae. A commonly used abbreviation is ❀ (‘leads to’):
Φ❀Φ =✷(Φ→✸Φ)
Here we have taken the liberty of using Φ→Φas an abbreviation for¬Φ∨Φ. Although strictly speaking ¬Φ is not part of the syntax, we consider¬to be a syntactic operation dualizing every operator in Φ ( and respectively
✸ and ✷ being dual), assuming that every propositional constant has an associated negated version.
Semantics of linear time logics is given with respect to runs through a transition system, i.e. as finite and infinite completed sequences of transi-tions.
Definition 4.2 Given a transition system T = (S, i, L,→) of typ e ·. For a transition (s, a, s)∈→definepre(s, a, s) = s, post(s, a, s) = s, lbl(s, a, s) = a. The set of(completed) runs Runss throughT starting ats∈S is defined as the set of pairs (s, δ) whereδ ∈Seq(→) is a sequence such that
(i) |δ|>0⇒pre(δ0) =s
(ii) ∀1≤i <|δ|. post(δi) =pre(δi+1) (iii) |δ|< ω∧post(δ|δ|)→ ⇒a a=∗
(iv) lbl(δi)=∗ Let Runs =
s∈SRunss be the set of all completed runs through T. For a run (s, δ) let init(s, δ) = s. ✷
The length of a run is the length of the underlying sequences, and the i’th
element and i’th suffix of a run is the i’th element and i’th suffix of the underlying sequence (with an initial state added for the suffix).
As adjacent transitions in a run are required to match by (ii) we can think of a run as an alternating sequences of states and actions, i.e.
s0a1s1. . . ansn
for the run (s0,(s0, a1, s1)(s1, a2, s2). . .(sn−1, an, sn)).
To summarize: Completed runs are finite or infinite sequences of idling transitions with a final state (if any) that cannot perform any non-idling actions.
Given a valuationV giving meaning to the propositional constantsp as sets V(p) of states, the semantics ΦT,V ⊆ Runs is defined by structural induction on Φ as follows (omitting subscriptsT and V for brevity):
p =
s∈V(p)Runss
Φ0∨Φ1 = Φ0 ∪ Φ1 Φ0∧Φ1 = Φ0 ∩ Φ1
Φ = {δ∈Runs|1≤ |δ|, δ1 ∈ Φ} Φ = {δ∈Runs| |δ|= 0 orδk∈ Φ}
✷Φ = {δ∈Runs| ∀k.|δ|< k or δk ∈ Φ}
✸Φ = {δ∈Runs| ∃k ≤ |δ|. δk ∈ Φ}
∃Φ = {δ∈Runs| ∃δ ∈Runsinit(δ). δ ∈ Φ}
∀Φ = {δ∈Runs| ∀δ ∈Runsinit(δ). δ ∈ Φ}
To compare this with formulas of the modal µ-calculus we need to define what it means for a state to satisfy a linear time formula. Here we have two possibilities:
s |=∃ Φ⇔def ∃δ∈Runss.δ∈ Φ or
s |=∀ Φ⇔def ∀δ∈Runss.δ∈ Φ
Notice, however, that for a formula with a path quantifier at the top-level the two definitions coincide as satisfaction of a path-quantified formula only depends on the first state of a run. We will refer to such formulae as state formulae and as a set of runs U with the property that if δ is a path in U
4.4 General Temporal properties 99 then all paths with the same initial state as δ also belongs to U, as having the state proverty. Formally:
Definition 4.3 A set U ⊆Runs has the state property if δ∈U ⇒(∀δ.init(δ) = init(δ)⇒δ ∈U.)
A formula Φ is a state formula if for all T andV, ΦT,V has the state prop-erty. ✷
For a state formulae Ψ we define
s |= Ψ⇔def s|=∃ Ψ(⇔s|=∀ Ψ) and we define
[[Ψ]] =def {s∈S | ∃δ∈Runss. δ∈ Ψ}
= {s∈S |s|= Ψ}
The translation of the full logic into the modal µ-calculus is quite in-volved due to the presence of assertions like: ∃(✸Φ0∧✸✷Φ1∧✷Φ2 ) which require various patterns of behaviour to hold for the same path. Dam [31]
describes one such translation. We consider instead a fragment of the logic – which we will refer to as CTL• (pronounced ‘CTL-dot’) – which at certain places requires the modalities to be under the scope of path quantifiers:
Ψ ::= p|Ψ∨Ψ|Ψ∧Ψ| ∃Ψ|
∀Ψ| ∃Ψ| ∀Ψ| ∃✷Φ| ∀✷Ψ| ∃✸Ψ| ∀✸Ψ| ∃✷✸Ψ| ∀✸✷Ψ This fragment is actually less restrictive than one might imagine at first sight. Using the equivalences of figure 4.4.1, many more (although far from all) assertions can be transformed into CTL•.
The embedding of a CTL• formula Ψ into the modal µ-calculus will be given as a function I defined recursively on the structure of Ψ. To describe the embedding we need a weak version of the diamond-modality . defined by .A = .A∨[.]F, and a strong version of the box-modality [.] defined by [.]A= [.]A∧ .T.
Figure 4.1: Some valid equivalences in CTL∗. In the last two lines of clauses Ψ is a CTL• formula. Equivalences involving the next operator also hold for the weak next operator.
I(p) = p
I(Ψ0∨Ψ1) = I(Ψ0)∨I(Ψ1) I(Ψ0∧Ψ1) = I(Ψ0)∧I(Ψ1)
I(∃ Ψ) = .I(Ψ) I(∀ Ψ) = [.]I(Ψ) I(∃ Ψ) = .I(Ψ) I(∀ Ψ) = [.]I(Ψ)
I(∃✷Ψ) = νX..X∧I(Ψ) I(∀✷Ψ) = νX.[.]X∧I(Ψ) I(∃✸Ψ) = µX..X∨I(Ψ) I(∀✸Ψ) = µX.[.]X∨I(Ψ)
I(∃✷✸Ψ) = νX.µY..Y ∨(.X∧I(Ψ)) I(∀✸✷Ψ) = µX.νY.[.]Y ∧([.]X∨I(Ψ))
Notice, thatI always yields closed assertions. Hence, the alternation depth of a translated formula I(Ψ) can easily seen to be one – or two when any of the assertions∃✷✸and ∀✸✷ are present in Ψ. It is interesting to note that the ‘dual’ variations3 ∀✷✸ and ∃✸✷of ∃✷✸ and ∀✸✷, yield translations
I(∀✷✸Ψ) =I(∀✷∀✸Ψ) =νX.[.]X∧(µY.[.]Y ∨I(Ψ)) and
3They arenot dual in the technical sense
4.4 General Temporal properties 101
I(∃✸✷Ψ) =I(∃✸∃✷Ψ) =µX..X∨(νY..Y ∧I(Ψ)) which are only of alternation depth one!
We can now prove:
Lemma 4.2 For all CT L• assertions Ψ and transition systems T with val-uation V, we have
[[Ψ]]T,V = [[I(Ψ)]]T,V
Proof: The proof is by structural induction on Ψ – the last two cases being a bit tricky, see appendix B.2. ✷
Operator CTL∗ Definition Meaning
EAlways(α, A) ∃✷ νX.αX∧A exists path on which always A
AAlways(α, A) ∀✷ νX.[α]X∧A on all paths alwaysA EEven(α, A) ∃✸ µX.αX∨A e.p.o.w. eventually A AEven(α, A) ∀✸ µX.[α]X∨A o.a.p. eventuallyA ERep(α, A) ∃✷✸ νX.µY.αY ∨(αX∧A) e.p.o.w. repeatingly A ARep(α, A) ∀✷✸ AAlways(α, AEven(α, A)) o.a.p. repeatinglyA EInfOften(α, A) νX.µY.αY ∨(αX∧A) e.p.o.w. infinitely oftenA AInfOften(α, A) νX.[α]X∧AEven(α, A) o.a.p. infinitely oftenA EEvenAlways(α, A) ∃✸✷ EEven(α, EAlways(α, A)) e.p.o.w. eventually alw. A AEvenAlways(α, A) ∀✸✷ µX.νY.[α]Y ∧([α]X∨A) o.a.p. eventually alw. A ELeadsTo(α, A, B) ∃❀ νX.αX∧ e.p.o.w. A alw. leads toB
(A→µY.αY ∨(X∧B))
ALeadsTo(α, A, B) ∀❀ AAlways(α o.a.p. A alw. leads to B A→AEven(α, B))
Table 4.1: Derived path operators. We will use EEven(A) as an abbre-viation for EEven(., A).
It is illustrative to write out the I translation of ∀(P ❀ Q). Notice first that ∀(P ❀ Q) =∀✷(P → ✸Q) = ∀✷∀(P → ✸Q) =∀✷(P → ∀✸Q). We now get
I(∀✷(P → ∀✸Q)) =νX.[.]X∧(P →µX.[.]X∨Q)
With this translation we can define a nice little collection of macros, which we systematically name asEAlwaysfor ‘there exists a path on which always . . . ’, and AAlways for ‘on all paths always . . . ’. To fit the general framework we generalize the translated assertions to allow for relativized ac-tions. Moreover, a slight anomaly arises in connection with the CTL assertion
✷✸, which is usually understood as ‘infinitely often’. With the semantics we have defined, this interpretation is only correct if attention is restricted to transition systems with total transition relations enforcing all maximal se-quences to be infinite. Instead of this rather unpleasant restriction on the models, we give two variations of pair of macros for ✷✸, one which requires the sequence to be infinite (EInfOften/AInfOften) and one which does not (ERep/ARep). Similar variations could be made of the other macros by re-moving or adding quotes. Table 4.1 shows the list of macros. Notice, that all assertions built using these macros will have alternation depth at most two. Figure 4.2 gives a visual explanation of some of the macros. The cones are to be thought of as the ‘computation tree’ of the underlying transition system with the initial state as the root.
This collection of macros includes the possibility of expressing what is known as safety properties (Always), liveness properties (Even), fairness properties (Rep/InfOften), and other progress properties like responsiveness (Leadsto). By combining these macros with constants and the abbreviations introduced in earlier chapters quite powerful assertions can be formed with-out having to “re-encode” directly in the modal µ-calculus.
Figure 4.2: Some of the path operators.
4.4 General Temporal properties 103 Example 4.9
1. “Whenever ab∗a has occurred we always end upwith a deadlock:”
AAlways([ab∗a]AEven(DeadLock)).
2. “Execution of a can always be followed in a finite number of steps by a b without performing any a’s:”
AAlways([a]AEven(Act\ {a},bT)).
3. “Requesting to get into a critical region by req will in a finite number of steps result in being in the critical region (denoted by the constant CR):”
AAlways([req]AEven(CR))
✷
Combining the characteristic formulas from section 4.3 with the macros de-fined here we can express some rather complicated properties:
Example 4.10
1. “Eventually this process will end up behaving weakly bisimilar to q:”
AEven(W/q).
2. “There exists a computation path on which it infinitely often will be possible to ready-simulate q:”
EInfOften(R/q).
3. “All the states that are ready bisimilar to q are also strongly bisimilar to r:”
AAlways((RB/q)→(B/r)).
4. “The pair of states that are weakly bisimilar but neither strongly bisim-ilar nor ready bisimbisim-ilar all belongs toAexcept if they both can perform ana:”
((W ∧ ¬B ∧ ¬RB)→A)∨ a×aT.
It is not obvious how useful such constructions are. But at least we are able to be more refined in our analysis than using an approach purely based on equational reasoning between specifications and implementations; we can for instance try to express properties about the states for which the equality fails or for instance change the equivalences to only consider certain actions or states. It is even possible to build in assumptions like: ‘Isp andq equivalent under the assumption that p and q are bisimilar?’ and so on. ✷