5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 65
Текст из файла (страница 65)
Dually, ∀ϕ holds in a state if all paths that start in that statesatisfy ϕ.Example 6.2.Legal CTL FormulaeLet AP = { x = 1, x < 2, x 3 } be a set of atomic propositions. Examples of syntacticallycorrect CTL formulae are∃ (x = 1), ∀ (x = 1), and x < 2 ∨ x = 1and ∃((x < 2) U (x 3)) and ∀(true U (x < 2)). Some examples of formulae that aresyntactically incorrect are∃(x = 1 ∧ ∀ (x 3)) and ∃ (true U (x = 1)).The first is not a CTL formula since x = 1 ∧ ∀ (x 3) is not a path formula and thusmust not be preceded by ∃. The second formula is not a CTL formula since true U (x = 1)is a path formula rather than a state formula, and thus cannot be preceded by .
Notethat∃ (x = 1 ∧ ∀ (x 3)) and ∃ ∀(true U (x = 1))are, however, syntactically correct CTL formulae.The Boolean operators true, false, ∧ , → and ⇔ are defined in the usual way. Thetemporal modalities “eventually”, “always”, and “weak until” can be derived—similarlyas for LTL—as follows:eventually: ∃♦Φ= ∃(true U Φ)∀♦Φ= ∀(true U Φ)always:∃Φ = ¬∀♦¬Φ∀Φ = ¬∃♦¬Φ∃♦ Φ is pronounced “Φ holds potentially” and ∀♦ Φ is pronounced “Φ is inevitable”. ∃ Φis pronounced “potentially always Φ”, ∀ Φ is pronounced “invariantly Φ”, and ∀ Φ ispronounced “for all paths next Φ”.Computation Tree Logic319Note that “always” Φ cannot be obtained from the “equation” Φ = ¬♦¬Φ (as in LTL),since propositional logic operators cannot be applied to path formulae.
In particular,∃¬♦¬Φ is not a CTL formula. Instead, we exploit the duality of existential and universalquantification:• there exists a path with the property E if and only if the state property “not allpaths violate property E” is satisfied, and• all paths satisfy property E if and only if the state property “there is a path withoutproperty E” is violated.Accordingly, ∃ Φ is not defined as ∃¬♦ ¬Φ, but rather as ¬∀♦ ¬Φ.Example 6.3.CTL FormulaeTo give a feeling about how simple properties can be formalized in CTL we treat someintuitive examples. The mutual exclusion property can be described in CTL by the formula∀(¬crit1 ∨ ¬crit2 ).CTL formulae of the form ∀∀♦Φ express that Φ is infinitely often true on all paths.(This fact will be formally proven later; see Remark 6.8 on page 326.) The CTL formula(∀∀♦crit1 ) ∧ (∀∀♦crit2 )thus requires each process to have access to the critical section infinitely often.
In caseof a traffic light, the safety property “each red light phase is preceded by a yellow lightphase” can be formulated in CTL by∀(yellow ∨ ∀ ¬red )depending on the precise meaning of a “phase”. The liveness property “the traffic light isinfinitely often green” can be formulated as∀∀♦green .Progress properties such as “every request will eventually be granted” can be describedby∀(request −→ ∀♦response).Finally, the CTL formula∀ ∃♦ startexpresses that in every reachable system state it is possible to return (via 0 or moretransitions) to (one of) the starting state(s).320Computation Tree Logic6.2.2SemanticsCTL formulae are interpreted over the states and paths of a transition system TS.
Formally, given a transition system TS, the semantics of CTL formulae is defined by twosatisfaction relations (both denoted by |=TS , or briefly |=): one for the state formulae andone for the path formulae. For the state formulae, |= is a relation between the states in TSand state formulae. We write s |= Φ rather than (s, Φ) ∈ |=. The intended interpretationis: s |= Φ if and only if state formula Φ holds in state s.
For the path formulae, |= isa relation between maximal path fragments in TS and path formulae. We write π |= Φrather than (π, Φ) ∈ |=. The intended interpretation is: π |= ϕ if and only if path πsatisfies path formula ϕ.Definition 6.4.Satisfaction Relation for CTLLet a ∈ AP be an atomic proposition, TS = (S, Act, →, I, AP, L) be a transition systemwithout terminal states, state s ∈ S, Φ, Ψ be CTL state formulae, and ϕ be a CTL pathformula.
The satisfaction relation |= is defined for state formulae bys |= aiffa ∈ L(s)s |= ¬ Φiffnot s |= Φs |= Φ ∧ Ψiff(s |= Φ) and (s |= Ψ)s |= ∃ϕiffπ |= ϕ for some π ∈ Paths(s)s |= ∀ϕiffπ |= ϕ for all π ∈ Paths(s)For path π, the satisfaction relation |= for path formulae is defined byπ |= Φiffπ[1] |= Φπ |= Φ U Ψiff∃ j 0. (π[j] |= Ψ ∧ (∀ 0 k < j. π[k] |= Φ)).where for path π = s0 s1 s2 . .
. and integer i 0, π[i] denotes the (i+1)th state of π, i.e.,π[i] = si .The interpretations for atomic propositions, negation, and conjunction are as usual, whereit should be noted that in CTL they are interpreted over states, whereas in LTL they areinterpreted over paths. state formula ∃ϕ is valid in state s if and only if there exists somepath starting in s that satisfies ϕ.
In contrast, ∀ϕ is valid in state s if and only if allpaths starting in s satisfy ϕ. The semantics of the path formulae is identical (althoughformulated slightly more simply) to that for LTL.1 For instance, ∃ Φ is valid in state s if1The semantics of the CTL path formulae is formulated more simply than for LTL, since in CTL eachComputation Tree Logic321and only if there exists some path π starting in s such that in the next state of this path,state π[1], the property Φ holds.
This is equivalent to the existence of a direct successors of s such that s |= Φ. ∀(Φ U Ψ) is valid in state s if and only if every path starting in shas an initial finite prefix (possibly only containing s) such that Ψ holds in the last stateof this prefix and Φ holds in all other states along the prefix. ∃(Φ U Ψ) is valid in s if andonly if there exists a path starting in s that satisfies Φ U Ψ. As for LTL, the semantics ofCTL here is nonstrict in the sense that the path formula Φ U Ψ is valid if the initial stateof the path satisfies Ψ.Definition 6.5.CTL Semantics for Transition SystemsGiven a transition system TS as before, the satisfaction set SatTS (Φ), or briefly Sat(Φ),for CTL-state formula Φ is defined by:Sat(Φ) = { s ∈ S | s |= Φ }.The transition system TS satisfies CTL formula Φ if and only if Φ holds in all initial statesof TS:TS |= Φ if and only if ∀s0 ∈ I.
s0 |= Φ .This is equivalent to I ⊆ Sat(Φ).The semantics of the derived path operators “always” and “eventually” is similar to thatin LTL. For path fragment π = s0 s1 s2 . . .:π |= ♦Φ if and only if sj |= Φ for some j 0.From this it can be derived that:s |= ∃Φ iff ∃π ∈ Paths(s). π[j] |= Φ for all j 0,s |= ∀Φ iff ∀π ∈ Paths(s). π[j] |= Φ for all j 0.Therefore, Φ can be understood as CTL path formula with the semantics:π = s0 s1 s2 . .
. |= Φif and only if sj |= Φ for all j 0.In particular, ∀Φ corresponds to the invariant over the invariant condition Φ.In a similar way, one can derive that ∃ Φ is valid in state s if and only if there existssome path starting at s such that for each state on this path the formula Φ holds.
Theformula ∃♦ Φ is valid in state s if and only if Φ holds eventually along some path thatstarts in s, and ∀♦ Φ is valid if and only if this property holds for all paths that start in s.A schematic overview of the validity of ∃, ∃♦, ∀♦, and ∀ is given in Figure 6.2, where322Computation Tree Logic∃♦ black∃ black∀♦ black∀ black∃(gray U black)∀(gray U black)Figure 6.2: Visualization of semantics of some basic CTL formulae.Computation Tree Logics3,1 up3323s2,1 up2s1,1 up1s0,1 up0s0,0downFigure 6.3: A transition system of the TMR system.PropertyPossibly the system never goes downFormalization in CTL∃ ¬ downInvariantly the system never goes down∀ ¬ downIt is always possible to start as new∀ ∃♦ up3The system always eventually goes downand is operational until going down∀ ((up3 ∨ up2 ) U down)Table 6.2: Some properties for the TMR system and their formalization in CTL.black-colored states satisfy the proposition black, gray states are labeled with gray, andall other states are labeled neither with black nor with gray.Example 6.6.A Triple Modular Redundant SystemConsider a triple modular redundant (TMR) system with three processors and a singlevoter.
As each component of this system can fail, the reliability is increased by lettingall processors execute the same program. The voter takes a majority vote of the outputsof the three processors. If a single processor fails, the system can still produce reliableoutputs. Each component can be repaired. It is assumed that only one component at atime can fail and only one at a time can be repaired. On failure of the voter, the entiresystem fails.
On repair of the voter, it is assumed that the system starts as being new,i.e., with three processors and a voter. The transition system of this TMR is depicted inFigure 6.3. States are of the form si,j where i denotes the number of processors that iscurrently up (0 < i 3) and j the number of operational voters (j = 0, 1). We consider theTMR system to be operational if at least two processors are functioning properly. Someinteresting properties of this system and their formulation in CTL are listed in Table 6.2on page 323.
We consider each of the formulae in isolation:temporal operator has to be immediately followed by a state formula.324Computation Tree Logic• state formula ∃ ¬ down holds in state s3,1 , as there is a path, e.g., (s3,1 s2,1 )ω ,starting in that state and that never reaches the down state, i.e., (s3,1 s2,1 )ω |= ¬ down.• Formula ∀ ¬ down, however, does not hold in state s3,1 , as there is a path startingfrom that state, such as (s3,1 )+ s0,0 . .
., that satisfies ¬ ¬ down, or, equivalently,♦ down.• Formula ∀ ∃♦ up3 holds in state s3,1 , as in any state of any of its paths it is possibleto return to the initial state, e.g., by first moving to state s0,0 and then to s3,1 . Forinstance, the path s3,1 (s2,1 )ω |= ∃♦ up3 since s2,1 |= ∃♦ up3,1 . This propertyshould not be confused with the CTL formula ∀♦ up3 , which expresses that eachpath eventually will visit the initial state.
(Note that this formula is trivially validfor state s3,1 as it satisfies up3 .)• The last property of Table 6.2 does not hold in state s3,1 as there exists a path,such as s3,1 s2,1 s1,1 s0,0 . . ., for which the path formula (up3 ∨ up2 ) U down doesnot hold. The formula is refuted since the path visits state s1,1 , a state that satisfiesneither down nor up3 nor up2 .Example 6.7.CTL SemanticsConsider the transition system depicted at the top (a) of Figure 6.4.
Just below thetransition system the validity of several CTL formulae is indicated for each state. (Forsimplicity, the initial states are not indicated.) A state is colored black if the formula isvalid in that state; otherwise, it is white. The following formulae are considered:• The formula ∃ a is valid for all states since all states have some direct successorstate that satisfies a.• ∀ a is not valid for state s0 , since a possible path starting at s0 goes directly tostate s2 for which a does not hold. Since the other states have only direct successorsfor which a holds, ∀ a is valid for all other states.• For all states except state s2 , it is possible to have a computation that leads to states3 (such as s0 s1 sω3 when starting in s0 ) for which a is globally valid.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
