Chapter 3 Questions.

Verification by Model Checking.

Interpretation of CTL formulas.

Question 1

Which of the specifications in plain English below convey the mathematical meaning of the CTL formula AG (p A[q U r]) ?
  1. Any reachable state in which p is true has a path from it on which r is eventually true, and until then q is true.
  2. If p is true in every reachable state, then there is a path along which q is continuously true, until r becomes true.
  3. If p is true in every reachable state, then for any path along which q is continuously true, r becomes true.
  4. For any reachable state in which p is true, then, on any path from that state, q is continuously true until r becomes true, and r is guaranteed to become true.
  5. If p is true in every reachable state, then on every path there is a state at which r is true, and q is true continuously until then.

Semantics of CTL.

Question 2

Consider the transition system (S, , L) where,

the set of states S equals {s0, s1, s2, s3};
the state transitions are (s0, s0), (s0, s1), (s0, s3), (s1, s2), (s2, s1) and (s3, s2); and
the labeling function is given by L(s0) = {r}, L(s1) = {p,r}, L(s2) = {q,r}, and L(s3) = {p,q}.

This model may be pictured as follows:

Which of the CTL formulas below are satisfied in state s0?
  1. AF (q r)
  2. AG (p AF (p r))
  3. A[r U q]
  4. AG(p AG(p q))
  5. AG EF r

Question 3

Which of the following pairs of CTL formulas are equivalent ?
  1. EF p and EG p
  2. EF p EF q and EF (p q)
  3. AF p AF q and AF (p q)
  4. AF p and A[p U ]
  5. EF p and AF p

Labelling algorithms.

Question 4

Apply the first labelling algorithm described in Section 3.5.1 of the textbook to check the formula E[r U AF q] of the model in Question 2. At the end of the algorithm, what is the set of formulas which will label s0?

  1. {r}
  2. {r, AF q}
  3. {r, E[r U q]}
  4. {r, E[r U AF q]}
  5. {r, AF q, E[r U AF q]}

SMV programs.

Question 5

Consider the SMV program fragment:

       MODULE main
       VAR
           a : boolean
           b : boolean
       ASSIGN
           init(a) := 0;
           init(b) := 0;
           next(a) := case
                        !a : 1;
                        1  : {0, 1};
                       esac;
           next(b) := case
                        !a : 0;
                        b  : 1;
                        1  : {0, 1};
                       esac;

Which of the following CTL models is adequately modelled by this SMV program fragment?

Question 6

Suppose we now add the program clause

FAIRNESS !a

to the SMV program fragment of Question 5. Which CTL formulas below (in isolation) hold for all inital states in the underlying model, according to the respective SMV run?
  1. AG (b AF a)
  2. AG AF b
  3. EG a
  4. AG EF b
  5. AG ( a EX b)

CTL*.

Question 7

Which of the following CTL* formulas are NOT expressible in CTL ?
  1. A[X p XX p]
  2. A[GF p F q]
  3. A[GF p]
  4. E[F p F q]
  5. A[G(p F q)]
Back to chapter index.