5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 72
Текст из файла (страница 72)
The fair paths starting in state s are defined asFairPaths(s) = {π ∈ Paths(s) | π |= fair }.Let FairPaths(TS) denote the set of all fair paths in TS, i.e.:FairPaths(s0 ).FairPaths(TS) =s0 ∈IThe fair interpretation of CTL is defined in terms of the satisfaction relation |=fair . Wehave s |=fair Φ if and only if Φ is valid in state s under the fairness assumption fair.Definition 6.33.Satisfaction Relation for CTL with FairnessLet TS = (S, Act, →, I, AP, L) be a transition system without terminal states and s ∈S. The satisfaction relation |=fair for CTL fairness assumption fair is defined for stateformulae bys |=fair aiffa ∈ L(s)s |=fair ¬ Φiffnot s |=fair Φs |=fair Φ ∧ Ψiff(s |=fair Φ) and (s |=fair Ψ)s |=fair ∃ϕiffπ |=fair ϕ for some π ∈ FairPaths(s)s |=fair ∀ϕiffπ |=fair ϕ for all π ∈ FairPaths(s)Here, a ∈ AP, Φ, Ψ are CTL state formulae, and ϕ a CTL path formula.
For path π, thesatisfaction relation |=fair for path formulae is defined as in Definition 6.4:π |=fair Φiffπ[1] |=fair Φπ |=fair Φ U Ψiff∃ j 0. (π[j] |=fair Ψ ∧ (∀ 0 k < j. π[k] |=fair Φ))Fairness in CTL361where for path π = s0 s1 s2 . . . and integer i 0, π[i] denotes the (i+1)-th state of π, i.e.,π[i] = si .Whereas for LTL, fairness constraints can be specified as part of the formula to be checked,for CTL similar constraints are imposed on the underlying model of the system underconsideration, i.e., the transition system.Definition 6.34.CTL Semantics with Fairness for Transition SystemsFor CTL-state formula Φ, and CTL fairness assumption fair, the satisfaction set Satfair (Φ)is defined bySatfair (Φ) = { s ∈ S | s |=fair Φ }.The transition system TS satisfies CTL formula Φ under fairness assumption fair if andonly if Φ holds in all initial states of TS:TS |=fair Φif and only if ∀s0 ∈ I.
s0 |=fair Φ.This is equivalent to I ⊆ Satfair (Φ).Example 6.35.CTL Fairness AssumptionConsider the transition system TS depicted in Figure 6.15 and suppose we are interested inestablishing whether or not TS |= ∀ (a ⇒ ∀♦ b). This formula is invalid since the paths0 s1 (s2 s4 )ω never goes through a b-state. The reason that this property is not valid is asfollows.
At state s2 there is a nondeterministic choice between moving either to state s3or to s4 . By continuously ignoring the possibility of going to s3 we obtain a computationfor which ∀ (a ⇒ ∀♦ b) is invalid, hence:TS |= ∀ (a ⇒ ∀♦ b).Usually, though, the intuition is that if there is infinitely often a choice of moving to s3 ,then s3 should be visited in some fair way.Let us impose the unconditional fairness assumption:fair ≡ ♦ a ∧ ♦ b.We now check ∀ (a ⇒ ∀♦ b) under fair, i.e., consider the verification problem TS |=fair∀ (a ⇒ ∀♦ b).
Due to the fairness assumption, paths like s0 s1 (s2 s4 )ω are excluded,since s3 is never visited along this path. It can now easily be established thatTS |=fair ∀ (a ⇒ ∀♦ b) .362Computation Tree Logic{b}s3s0s1s2{a}{a}{a}s4{a}Figure 6.15: An example of a transition system.Example 6.36.Mutual ExclusionConsider the semaphore-based solution to the two-process mutual exclusion problem. Thetransition system of this concurrent program is denoted TSsem . The CTL formulaΦ = (∀ ∀♦ crit1 ) ∧ (∀ ∀♦ crit2 )describes the liveness property that both processes infinitely often have access to thecritical section.
It follows that TSsem |= Φ. We first impose the weak fairness assumptionwfair = (♦ noncrit1 → ♦ wait1 ) ∧ (♦ noncrit2 → ♦ wait2 )and the strong fairness assumptionsfair = ( ♦ wait1 → ♦ crit1 ) ∧ ( ♦ wait1 → ♦ crit1 ) .It then follows that TSsem |=fair Φ where fair = wfair ∧ sfair .As a second example, consider the arbiter-based solution to the two-process mutual exclusion problem, see Example 5.27 on page 259.
The decision as to which process will acquireaccess to the critical section is determined by coin flipping by the arbiter. Consider theunconditional fairness assumptionufair = ♦ head ∧ ♦ tail .This fairness assumption can be considered to require a fair coin such that the events“heads” and “tails” occur infinitely often with probability 1. Apparently, it follows thatTS1 Arbiter TS2 |= Φ,and TS1 Arbiter TS2 |=ufair Φ.Fairness in CTL363As explained before, fairness is treated in CTL by considering a fair satisfaction relation,denoted |=fair where fair is the fairness assumption considered. In the remainder of thissection, algorithms will be provided in order to check whetherTS |=fair Φfor CTL formula Φ and CTL-fairness assumption fair.
As before, TS is supposed tobe finite and have no terminal states and Φ is a CTL formula in ENF. Note that theassumption that Φ is in ENF does not impose any restriction as any CTL formula can betransformed into an equivalent (with respect to |=fair ) CTL formula in ENF. This can beestablished in the same way as Theorem 6.14 (page 332).The basic idea is to exploit the CTL model-checking algorithms (without fairness) tocompute Satfair (Φ) = { s ∈ S | s |=fair Φ }.
Suppose fair is the strong CTL fairnessconstraint:( ♦ Φi → ♦ Ψi )fair =0<ikwhere Φi and Ψi are CTL formulae over AP. Recall that Φi and Ψi are interpretedaccording to the standard CTL semantics, i.e., without taking any fairness assumptionsinto account.
By applying the CTL model-checking algorithm, first the sets Sat(Φi ) andSat(Ψi ) are determined. The formulae Φi and Ψi can thus be replaced by (fresh) atomicpropositions ai and bi , say. It thus suffices to consider strong fairness assumptions of theform( ♦ ai → ♦ bi ) .fair =0<ikOnce the fairness assumption is simplified, the sets Satfair (Ψ) are determined for all subformulae Ψ of Φ using the standard CTL model-checking algorithm (i.e., without fairness),together with an algorithm to compute Satfair (∃ a) for a ∈ AP . The outcome of themodel-checking procedure is “yes” if I ⊆ Satfair (Φ), and “no” otherwise.The essential ideas are outlined in Algorithm 17 (page 364).The subformulae of Φ are treated as in the CTL model-checking routine.
Based on thesyntax tree of Φ, a bottom-up computation is initiated. It is essential that during thecomputation of Satfair (Ψ), the maximal genuine subformulae of Ψ have been alreadyprocessed and replaced by atomic propositions. For the propositional logic fragment,364Computation Tree LogicAlgorithm 17 CTL model checking with fairness (basic idea)Input: finite transition system TS, CTL formula Φ in ENF, and CTL fairness assumption fair overk CTL state formulae Φi and ΨiOutput: TS |=fair Φfor all 0 < i k dodetermine Sat(Φi ) and Sat(Ψi )if s ∈ Sat(Φi ) then L(s) := L(s) ∪ { ai }; fiif s ∈ Sat(Ψi ) then L(s) := L(s) ∪ { bi }; fiodcompute Satfair (∃ true) = { s ∈ S | FairPaths(s) = ∅ };forall s ∈ Satfair (∃ true) do L(s) := L(s) ∪ { afair ; } od(* compute Satfair (Φ) *)for all i | Φ | dofor all Ψ ∈ Sub(Φ) with | Ψ | = i doswitch(Ψ):true: Satfair (Ψ) := S;a: Satfair (Ψ) := { s ∈ S | a ∈ L(s) };a ∧ a: Satfair (Ψ) := { s ∈ S | a, a ∈ L(s) };¬a: Satfair (Ψ) := { s ∈ S | a ∈ L(s) };∃ a: Satfair (Ψ) := Sat(∃ (a ∧ afair ));∃(a U a ) : Satfair (Ψ) := Sat(∃(a U (a ∧ afair )));∃ a: compute Satfair (∃ a)end switchreplace all occurrences of Ψ in Φ by the atomic proposition aΨ ;forall s ∈ Satfair (Ψ) do L(s) := L(s) ∪ { aΨ } odododreturn I ⊆ Satfair (Φ)Fairness in CTL365the approach is straightforward:Satfair (true)Satfair (a)Satfair (¬a)Satfair (a ∧ a )====S{ s ∈ S | a ∈ L(s) }S \ Satfair (a)Satfair (a) ∩ Satfair (a ).For all nodes of the syntax tree that are labeled with either ∃ or ∃ U (i.e, nodes thatrepresent a subformula of the form Ψ = ∃ a or of the form Ψ = ∃(a U a )), the followingobservation is used.
For any infinite path fragment π in TS, π is fair if and only if one (orall) suffix(es) of π is (are) fair:π |= fairiffπ[j..] |= fair for some j 0iffπ[j..] |= fair for all j 0.The following two lemmas provide the ingredients for checking subformulae of the “type”∃ and ∃ U.Lemma 6.37.Next Step for Fair Satisfaction Relations |=fair ∃ a if and only if ∃s ∈ Post(s) with s |= a and FairPaths(s ) = ∅.Proof: ⇒: Assume s |=fair ∃ a.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
