5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 88
Текст из файла (страница 88)
Decidewhether TS |= Φi for i = 1, 2 using the CTL model-checkingalgorithm. Sketch its main steps.s1 { a, b }s2{c}s3{ b, c }s4{c}Exercise 6.17. Provide an algorithm in pseudo code to compute Sat(∀(Φ U Ψ)) in a directmanner, i.e., without transforming the formula into ENF.Exercise 6.18.(a) Prove that Sat(∃(Φ W Ψ)) is the largest set T such thatT ⊆ Sat(Ψ) ∪ s ∈ Sat(Φ) | Post(s) ∩ T = ∅ .(b) Prove that Sat(∀(Φ W Ψ)) is the largest set T such thatT ⊆ Sat(Ψ) ∪ s ∈ Sat(Φ) | Post(s) ⊆ T .438Computation Tree LogicUse the above characterizations to provide efficient algorithms for computing the sets Sat(∃(Φ W Ψ))and Sat(∀(Φ W Ψ)) in a direct manner.Exercise 6.19.
Consider the fragment ECTL of CTL which consists of formulae built accordingto the following grammar:Φ ::= a | ¬a | Φ ∧ Φ | ∃ϕϕ::= Φ | Φ | Φ U ΦFor two transition systems TS1 = (S1 , Act, →1 , I1 , AP, L1 ) and TS2 = (S2 , Act, →2 , I2 , AP, L2 ),let TS1 ⊆ TS2 iff S1 ⊆ S2 , →1 ⊆ →2 , I1 = I2 and L1 (s) = L2 (s) for all s ∈ S1 .(a) Prove that for all ECTL formulae Φ and all transition systems TS1 , TS2 with TS1 ⊆ TS2 ,it holds:TS1 |= Φ=⇒TS2 |= Φ.(b) Give a CTL formula which is not equivalent to any other ECTL formula.
Justify youranswer.Exercise 6.20. In CTL, the release operator is defined by∃(Φ R Ψ) = ¬∀((¬Φ) U (¬Ψ))and∀(Φ R Ψ) = ¬∃((¬Φ) U (¬Ψ)).(a) Provide expansion laws for ∃(Φ R Ψ) and ∀(Φ R Ψ).(b) Give a pseudo code algorithm for computing Sat(∃(Φ R Ψ)) and do the same for computingSat(∀(Φ R Ψ)).Exercise 6.21. Consider the CTL formula Φ and the strong fairness assumption sfair :Φ= ∀ ∀♦ asfair= ♦ (b ∧ ¬a) → ♦ ∃ (b U (a ∧ ¬b)) Φ1and transition system TS over AP = { a, b } which is given byΨ1Exercises439{ a, b }s0{ b } s3s1∅s2 { b }s4∅s5 { a }Questions:(a) Determine Sat(Φ1 ) and Sat(Ψ1 ) (without fairness).(b) Determine Satsfair (∃ true).(c) Determine Satsfair (Φ).Exercise 6.22. Let TS = (S, Act, →, I, AP, L) be a transition system without terminal states,a, b ∈ AP and s ∈ S.
Furthermore, let fair be a CTL fairness assumption and afair ∈ AP anatomic proposition with afair ∈ L(s) iff s |=fair ∃true.Which of the following assertions are correct? Give a proof or counterexample.(a) s |=fair ∀(a U b) iffs |= ∀(a U (b ∧ afair )).(b) s |=fair ∃(a W b) iff s |= ∃(a W (b ∧ afair )).(c) s |=fair ∀(a W b) iff s |= ∀(a W (afair → b)).Exercise 6.23. Consider the following transition system TS over AP = { a1 , . . . , a6 }.{ a 1 , a3 }s2{ a 4 , a2 }s3∅s1{ a1 }s5{ a 1 , a2 } { a 2 , a4 }s6s4s7{ a 1 , a5 }{ a 3 , a2 , a5 }s8440Computation Tree LogicLet Φ = ∃ a1 → ∃(a1 U a2 ) and sfair = sfair 1 ∧ sfair 2 ∧ sfair 3 a strong CTL fairnessassumption wheresfair 1=♦ ∀♦(a1 ∨ a3 ) −→ ♦a4sfair 2sfair 3==♦(a3 ∧ ¬a4 ) −→ ♦a5♦(a2 ∧ a5 ) −→ ♦a6Sketch the main steps for computing the satisfaction sets Satsfair (∃true) and Satsfair (Φ).Exercise 6.24.
Consider the CTL∗ formula over AP = { a, b }:Φ = ∀♦ ∃ a U ∃ band the transition system TS outlined below:{b}s0{ a, b } s2s5s1 ∅{ a } s3∅s6{ a, b }s4 { b }s7{ a, b }Apply the CTL∗ model-checking algorithm to compute Sat(Φ) and decide whether TS |= Φ. (Hint:You may infer the satisfaction sets for LTL formulae directly.)Exercise 6.25. The model-checking algorithm presented in Section 6.5 treats CTL with strongfairness assumptions.
Explain which modifications are necessary to deal with weak CTL fairnessassumptions: wfair =♦ai −→ ♦bi .1ikYou may assume that ai , bi ∈ { true } ∪ AP.Exercise 6.26. Which of the following equivalences for CTL∗ are correct? Provide a proof or acounterexample.Exercises441(a) ∀ ∀Φ ≡ ∀ Φ(b) ∃ ∃Φ ≡ ∃ Φ(c) ∀(ϕ ∧ ψ) ≡ ∀ϕ ∧ ∀ψ(d) ∃(ϕ ∧ ψ) ≡ ∃ϕ ∧ ∃ψ(e) ¬∀(ϕ → ψ) ≡ ∃(ϕ ∧ ¬ψ)(f) ∃∃ Φ ∧ ¬∀ ¬Φ ≡ ∃(¬ ¬Φ)(g) ∀(♦Ψ ∧ Φ) ≡ ∀♦(Ψ ∧ ∀Φ) ∧ ∀(Φ ∧ ∀♦Ψ)(h) ∃(♦Ψ ∧ Φ) ≡ ∃♦(Ψ ∧ ∃Φ)Here, Φ, Ψ are arbitrary CTL∗ state formulae and ψ, ϕ are CTL∗ path formulae.Exercise 6.27.Consider the transition system TS and the CTL∗ formulaΦ = ∃ (a ∧ ¬b) ∧ ∀ (b U a) .Apply the CTL∗ model-checking algorithm to checkwhether TS |= Φ and sketch its main steps as well as itsoutput. (Hint: You may compute the LTL satisfaction setsdirectly.){b}s0{ a, b }s1{ a } s2s3{a}s4{ a, b }Exercise 6.28.
Consider the transition system TS depicted below and the CTL∗ formulaΦ = ∃ (♦b ∧ ∃♦ a) ∧ ∀♦ c.{c}s2s1∅{a}s4∅s3s5{b, c}Sketch the main steps that the CTL∗ model checking algorithm performs for checking whetherTS |= Φ.442Computation Tree LogicExercise 6.29. Provide an example of a CTL∗ formula which is not a CTL+ formula, but thereexists an equivalent CTL formula.Exercise 6.30. Provide equivalent CTL formulae for the CTL+ formulae ∀(♦a∧b) and ∀( a∧¬(a U (b))).Practical ExercisesThe remaining exercises are modeling and veriifcation exercises using the CTL model checkerNuSMV [83].Exercise 6.31.
The following program is a mutual exclusion protocol for two processes due toPnueli (taken from [118]). There is a single shared variable s which is either 0 or 1, and initiallyequals 1. Besides, each process has a local Boolean variable y that initially equals 0. The programtext for process Pi (i = 0, 1) is as follows:l0: loop forever dobeginl1: Noncritical sectionl2: (yi , s) := (1, i);l3: wait until ((y1−i = 0) ∨ (s = i));l4: Critical sectionl5: yi := 0end.Here, the statement (yi , s) := (1, i) is a multiple assignment in which variable yi := 1 and s := i isa single, atomic step.The intuition behind this protocol is as follows. The variables y0 and y1 are used by each process tosignal the other process of active interest in entering the critical section. On leaving the noncriticalsection, process Pi sets its own local variable yi to 1.
In a similar way this variable is reset to 0once the critical section is left. The global variable s is used to resolve a tie situation between theprocesses. It serves as a logbook in which each process that sets its y variable to 1 signs at thesame time. The test at line l3 says that P0 may enter its critical section if either y1 equals 0 –implying that its competitor is not interested in entering its critical section – or if s differs from0 – implying that the competitor process P1 performed its assignment to y1 after p0 assigned 1 toy0 .Questions concerning this mutual exclusion protocol:(a) Model this protocol in NuSMV; formulate the property of mutual exclusion in CTL andcheck this property.Exercises443(b) Check whether Pnueli’s protocol ensures absence of unbounded overtaking, i.e., when aprocess wants to enter its critical section, it eventually will be able to do so.
Provide acounterexample (and an explanation thereof) in case this property is violated.(c) Add the fairness constraint FAIRNESS running to the process specification in your NuSMVmodel of the mutual exclusion program, and check again the property of absence of unbounded overtaking. Compare the obtained results with the results obtained in the previousquestion without using the fairness constraint.(d) Express in CTL that each process will occupy its critical section infinitely often.
Check theproperty (use again the FAIRNESS running).(e) A practical problem with this mutual exclusion protocol is that it is too demanding in thesense that it enforces performing the assignments to yi and s (in line l2) in a single step.Most existing hardware systems cannot perform such assignments in one step. Therefore,it is requested to investigate whether any of the four possible realizations of this protocol– in which the aforementioned assignments are not atomic anymore – is a correct mutualexclusion protocol.(I) Report for each possible implementation your results, including possible counterexamples and their explanation.(II) Compare your results with the results of your Promela experiments with this exercisein the previous exercise series.Exercise 6.32. In this exercise you are confronted with a nonstandard example for modelchecking. The purpose of this exercise is to present the model checker as a solver for combinatorialproblems rather than a tool for correctness analysis.
These problems involve a search (involvingbacktracking) of optimal or cost-minimizing strategies such as schedulers or puzzle solutions. Theexercise is concerned with Loyd’s puzzle that consists of an N · K grid in which there are N · K−1numbered tiles and a single blank space.
The goal of the puzzle is to achieve a predetermined orderon the tiles. The initial and final configuration of the tiles for N = 3 and K = 3 is as follows:1287634554367821initial configurationfinal configurationNote that there are approximately 4 · (N · K)! possible moves in this puzzle. For N = 3 and K = 3this already amounts to about 1.45 106 possible configurations.Questions concerning Loyd’s puzzle:444Computation Tree Logic(a) Complete the (partial) model of Loyd’s puzzle in NuSMV that is given below.
In this model,there is an array h that keeps track of the horizontal positions of the tiles and an array vthat records the vertical positions of the tiles such that the position of tile i is given by thepair h[i], v[i]. Tile 0 represents the blank tile. Position h[i] = 1 and v[i] = 1 is thelowest left corner of the puzzle.MODULE mainDEFINE N := 3; K := 3;VAR move: {u, d, l, r};h: array 0..8 of 1..3;v: array 0..8 of 1..3;-- the possible tile-moves-- the horizontal positions of all tiles-- ....
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
