5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 87
Текст из файла (страница 87)
CTL model checking basedon a forward search has been proposed by Iwashita, Nakata, and Hirose [224]. Emersonand Lei [143] showed that CTL∗ can be checked with essentially the same complexity asLTL, using a combination of the algorithms for LTL and CTL. The same authors considerin [142] CTL model checking under a broad class of fairness assumptions. Practical aspectsof CTL∗ model checking have been reported by Bhat, Cleaveland, and Grumberg [50], andmore recently by Visser and Barringer [414]. Algorithms for generating counterexamplesand witnesses originate from the works by Clarke et al. [91] and Hojati, Brayton, andKurshan [204].
More recent developments are the use of satisfiability solvers for propositional logic or quantified Boolean formulae to find counterexamples up to certain length,as proposed by Clarke et al. [84], and the use of tree-like counterexamples as opposed tolinear ones by Clarke [93].CTL model checkers. Clarke and Emerson [86] reported the first (fair) CTL model checker,called EMC. About the same time, Queille and Sifakis [347] announced CESAR, a modelchecker for a branching logic very similar to CTL.
EMC was improved in [87] and constituted the basis for SMV (Symbolic Model Verifier), an efficient CTL model checker byMcMillan based on a symbolic OBDD-based representation of the state space [288]. Theconcept of ordered binary decision diagrams has been proposed by Bryant [70]. The milestone for symbolic model checking with OBDDs is the paper by Burch et al.[74]. Furtherreferences for OBDD-based approaches have been given in Section 6.7.
Recent variantsof SMV are NuSMV [83] developed by the teams of Cimatti et al., and SMV by McMillan and colleagues at Cadence Berkeley Laboratories that is focused on compositionality.Both tools are freely available. Another symbolic CTL model checker is VIS [62].Exercises6.11433ExercisesExercise 6.1. Consider the following transition system over AP = { b, g, r, y }:{y}132{g}{r}4{b}The following atomic propositions are used: r (red), y (yellow), g (green), and b (black). Themodel is intended to describe a traffic light that is able to blink yellow.
You are requested toindicate for each of the following CTL formulae the set of states for which these formulae hold:Exercise 6.2.the right:(a)∀♦ y(g)∃ ¬ g(b)∀ y(h)∀(b U ¬ b)(c)∀ ∀♦ y(i)∃(b U ¬ b)(d)∀♦ g(j)∀( ¬ b U ∃♦ b)(e)∃♦ g(k)∀(g U ∀(y U r))(f)∃ g(l)∀( ¬ b U b)Consider the following CTL formulae and the transition system TS outlined onΦ1= ∀(a U b) ∨ ∃ (∀ b)Φ2= ∀ ∀(a U b)Φ3= (a ∧ b) → ∃ ∃ ∀(b W a)Φ4= (∀ ∃♦ Φ3 )s0∅s4{b}s3s2s1{b}{ a, b }{a}Determine the satisfaction sets Sat(Φi ) and decide whether TS |= Φi (1 i 4).Exercise 6.3. Which of the following assertions are correct? Provide a proof or a counterexample.(a) If s |= ∃ a, then s |= ∀ a.(b) If s |= ∀ a, then s |= ∃ a.(c) If s |= ∀♦ a ∨ ∀♦ b, then s |= ∀♦ (a ∨ b).(d) If s |= ∀♦ (a ∨ b), then s |= ∀♦ a ∨ ∀♦ b.434Computation Tree Logic(e) If s |= ∀(a U b), then s |= ¬ (∃(¬b U (¬a ∧ ¬b)) ∨ ∃ ¬b).Exercise 6.4.
Let Φ and Ψ be arbitrary CTL formulae. Which of the following equivalences forCTL formulae are correct?(a) ∀ ∀♦ Φ ≡ ∀♦ ∀ Φ(b) ∃ ∃♦ Φ ≡ ∃♦ ∃ Φ(c) ∀ ∀ Φ ≡ ∀ ∀ Φ(d) ∃ ∃ Φ ≡ ∃ ∃ Φ(e) ∃♦ ∃ Φ ≡ ∃ ∃♦ Φ(f) ∀ (Φ ⇒ (¬Ψ ∧ ∃ Φ)) ≡ (Φ ⇒ ¬∀♦ Ψ)(g) ∀ (Φ ⇒ Ψ) ≡ (∃ Φ ⇒ ∃ Ψ)(h) ¬∀(Φ U Ψ) ≡ ∃(Φ U ¬Ψ)(i) ∃((Φ ∧ Ψ) U (¬Φ ∧ Ψ)) ≡ ∃(Φ U (¬Φ ∧ Ψ))(j) ∀(Φ W Ψ) ≡ ¬∃(¬Φ W ¬Ψ)(k) ∃(Φ U Ψ) ≡ ∃(Φ U Ψ) ∧ ∃♦Ψ(l) ∃(Ψ W ¬Ψ) ∨ ∀(Ψ U false) ≡ ∃ Φ ∨ ∀ ¬Φ(m) ∀Φ ∧ (¬Φ ∨ ∃ ∃♦¬Φ) ≡ ∃X¬Φ ∧ ∀ Φ(n) ∀∀♦Φ ≡ Φ ∧ (∀ ∀∀♦Φ) ∨ ∀ (∀♦Φ ∧ ∀∀♦Φ)(o) ∀Φ ≡ Φ ∨ ∀ ∀ΦExercise 6.5. Consider an elevator system that services N > 0 floors numbered 0 through N −1.There is an elevator door at each floor with a call button and an indicator light that signals whetheror not the elevator has been called.
In the elevator cabin there are N send buttons (one per floor)and N indicator lights that inform to which floor(s) is going to be sent. For simplicity considerN = 4. Present a set of atomic propositions—try to minimize the number of propositions—thatare needed to describe the following properties of the elevator system as CTL formulae and givethe corresponding CTL formulae:(a) The doors are “safe”, i.e., a floor door is never open if the cabin is not present at the givenfloor.(b) The indicator lights correctly reflect the current requests. That is, each time a button ispressed, there is a corresponding request that needs to be memorized until fulfillment (ifever).(c) The elevator only services the requested floors and does not move when there is no request.Exercises435(d) All requests are eventually satisfied.Exercise 6.6.
Consider the single pulser circuit, a hardware circuit that is part of a set ofbenchmark circuits for hardware verification. The single pulser has the following informal specification: “For every pulse at the input inp there appears exactly one pulse of length 1 at outputoutp, independent of the length of the input pulse”. Thus, the single pulser circuit is required togenerate an output pulse between two rising edges of the input signal. The following questionsrequire the formulation of the circuit in terms of CTL. Suppose we have the proposition rise edgeat our disposal which is true if the input was low (0) at time instant n−1 and high (1) at timeinstant n (for natural n > 0).
It is assumed that input sequences of the circuit are well behaved,i.e., more that the rising edge appears in the input sequence.Questions: specify the following requirements of the circuit in CTL:(a) A rising edge at the inputs leads to an output pulse.(b) There is at most one output pulse for each rising edge.(c) There is at most one rising edge for each output pulse.(This exercise is taken from [246].)Exercise 6.7. Transform the following CTL formulae into ENF and PNF. Show all intermediatesteps.Φ1 = ∀ (¬a) W (b → ∀ c)Φ2=∀∃((¬a) U (b ∧ ¬c)) ∨ ∃ ∀ aExercise 6.8.
Provide two finite transition systems TS1 and TS2 (without terminal states,and over the same set of atomic propositions) and a CTL formula Φ such that Traces(TS1 ) =Traces(TS2 ) and TS1 |= Φ, but TS2 |= Φ.Exercise 6.9. Consider the CTL formulaΦ = ∀ a → ∀♦ (b ∧ ¬a)and the following CTL fairness assumption:fair = ∀♦ ∀ (a ∧ ¬b) → ∀♦ ∀ (b ∧ ¬a) ∧ ♦ ∃♦ b → ♦ b.Prove that TS |=f air Φ where transition system TS is depicted below.436Computation Tree Logic∅s0{a}s1s3{a}s4{ a, b }{b}s2Exercise 6.10.
Let ℘ = (z1 , z2 , z3 , z4 , z5 , z6 ). Depict the ℘-ROBDD for the majority function1if b1 + b2 + . . . + b6 4MAJ([z1 = b1 , z2 = b2 , . . . , z6 = b6 ]) =0otherwise.Exercise 6.11. Consider the functionwhere n = 2k , and m =k−1j=0F (x0 , . . . , xn−1 , a0 , .
. . , ak−1 ) = xmaj 2j . Let k=3. Questions:(a) Depict the ℘-ROBDD for ℘ = (a0 , . . . , ak−1 , x0 , . . . , xn−1 ).(b) Depict the ℘-ROBDD for ℘ = (a0 , x0 , . . . , ak−1 , xk−1 , xk , . . . , xn−1 ).Exercise 6.12. Let B and C be two ℘-ROBDDs. Design an algorithm that checks whetherfB = fC and runs in time linear in the sizes of B and C.(Hint: It is assumed that B and C are given as separate graphs (and not by nodes of a sharedOBDD).)Exercise 6.13. Let TS be a finite transition system (over AP) without terminal states, and Φand Ψ be CTL state formulae (over AP).
Prove or disproveTS |= ∃(Φ U Ψ) if and only ifTS |= ∃♦ Ψwhere TS is obtained from TS by eliminating all outgoing transitions from states s such thats |= Ψ ∨ ¬Φ.Exercise 6.14. Check for each of the following formula pairs (Φi , ϕi ) whether the CTL formulaΦi is equivalent to the LTL formula ϕi . Prove the equivalence or provide a counterexample thatillustrates why Φi ≡ ϕi .Exercises437(a) Φ1 = ∀∀ a.
and ϕ1 = a(b) Φ2 = ∀♦∀ a and ϕ2 = ♦ a.(c) Φ3 = ∀♦(a ∧ ∃ a) and ϕ3 = ♦(a ∧ a).(d) Φ4 = ∀♦a ∨ ∀♦b and ϕ4 = ♦(a ∨ b).(e) Φ5 = ∀(a → ∀♦b) and ϕ5 = (a → ♦b).(f) Φ6 = ∀(b U (a ∧ ∀b)) and ϕ6 = ♦a ∧ b.Exercise 6.15.(a) Prove, using Theorem 6.18, that there does not exist an equivalent LTL formula for the CTLformula Φ1 = ∀♦ (a ∧ ∃ a).(b) Now prove directly (i.e.
without Theorem 6.18), that there does not exist an equivalent LTLformula for the CTL formula Φ2 = ∀♦ ∃ ∀♦ ¬a. (Hint: Argument by contraposition.)Exercise 6.16.s0 { a }Consider the following CTL formulaeΦ1 = ∃♦ ∀ candΦ2 = ∀(a U ∀♦ c)and the transition system TS outlined on the right.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
