辅导 COMP3153/9153 Algorithmic Verification Final Take-Home Exam Term 2, 2023调试数据库编程

COMP3153/9153

Algorithmic Verification

Final Take-Home Exam

Term 2, 2023

Question 1 (10 marks)

Consider the following automaton C:

For each of the following CTL* formulae, determine whether C satisfies it or not. Justify your answers.

(a) (F q) → (Gp)

(b) (F Gp) → (G F q)

(d) AG (p → AX q)

(e) G ((X q) ∨ (pUr))

Question 2 (10 marks)

Consider the automaton C from the previous question. The labelling function defines an abstraction, A, of C where the states of A are given by the values of the atomic propostions p, q, and r. For example, because L(q1 ) = L(q3 ), states q1 and q3 would map to the same abstract state.

(a) Draw A.

(b) Are A and C bisimilar? Justify your answer.

(d) Refine the abstraction of A based on φ . That is, find a model A′ such that A ⊑ A′ ⊑ C and A′ |= φ if and only if C |= φ . Try to find a model A′ ≠ C, or explain why this is not possible.

Question 3 (10 marks)

For each of the following pairs of LTL or CTL formulas, prove or disprove whether they are equivalent. That is, prove or disprove for all models M, M |= φ 1 if and only if M |= φ2

(a) φ 1 = G (F (pU q)) and φ2 = G (F q)

(b) φ 1 = (Fp) Uq and φ2 = (Fp) ∧ (F q)

(d) φ 1 = X (pU (Gq)) and φ2 = G ((Xp)U (Gq))

(e) φ 1 = (Xp)U (X (pU q)) and φ2 = (X (pU q))U (X q)

Question 4 (15 marks)

We extend LTL by a Before operator. Its semantics are given as

ρ |= φBefore ψ ⇐⇒ (∀k ≥ 0. (ρ[k] |= ψ) =⇒ (∃j. 0 ≤ j ≤ k ∧ ρ[j] |= φ)) .

(a) Briefly describe in your own words the meaning of Before.

(b) Prove that the Before operator does not extend the expressiveness of LTL. That is, give an LTL formula that is equivalent to φBefore ψ and argue their equiva- lence.

i. ((pBefore q) ∧ q) implies p;

ii. p Before (q ∨ r) is equivalent to ((pBefore q) ∧ (pBefore r)).

(d) Give a B¨uchi automaton that accepts the words described by the formula p Before q

(e) How could you extend the LTL model checking algorithm to handle the Before operator directly?

(f) If we add the Before operator to the path formulae of CTL in the obvious way, explain how to extend the CTL model checking algorithm to handle E(·Before ·) subformulae directly.

Question 5 (15 marks)

(a) Give OBDDs for the following boolean functions:

i. f(x,y, z) = (x ∧ y ∧ z) ∨ (¬x ∧ ¬y ∧ ¬z)

ii. f(x,y, z) = (x ∨ y) ∧ (y ∨ z) ∧ (z ∨ x)

(b) Consider the following OBDD describing the boolean function T(x0 , x1 , x0(′), x1(′)):

Here a solid line indicates the Boolean value true, and a dashed line the value false.

T(x0 , x1 , x0(′), x1(′)) defines a transition relation of a four state automaton where the states are given by pairs of boolean values (i.e. Q = {00, 01, 10, 11}). with a transition between q and q′ if and only if T(q, q′ ) = true.

Draw this automaton.

(c) How can you use OBDDs to solve the SAT problem? That is, given an OBDD for boolean formula φ , Dφ , how can you find an assignment of true/false to the variables of φ which makes φ true?

(d) Prove or disprove: If D1 and D2 are OBDDs on n variables with O(n) nodes, then D1 ⊗ D2 has O(n) nodes.

Question 6 (10 marks)

Consider the following decorated pseudo-code program written in a simple imperative programming language:

[ a := x +b ]1 ;

[ y := a *b ]2 ;

while [y > a + b ]3 do (

[ x := a +1]4 ;

[ y := a +b ]5 ;

if [( a +1 > a +b )]6 :

[ a := x +1]7 ;

else :

[ x := a +1]8 ;

);

(a) Give a control flow graph for this program. The code decorations given by [ ..]# indicate the eight critical states to include in the graph.

(b) Give the table of gen and kill sets for an live variable analysis of the program.

Question 7 (10 marks)

Consider the LTL formula:

φ = G (pU q)

Let Σ = 2{p,q} = {∅ , {p}, {q}, {p,q}}

(a) Give a B¨uchi automaton that accepts the words (in Σω ) described by φ . Justify your construction.

(b) Give a B¨uchi automaton that accepts the words (in Σω ) described by ¬φ . Justify your construction.

(c) Give a safety property Ps and aliveness property Pe such that the set of behaviours described by φ is equal to Ps ∩ Pe.

Question 8 (20 marks)

Consider the network of timed automata depicted in Figure 1.

Figure 1: System of Traffic Lights

The automata describe a system of traffic lights. The syntax is as follows: green statements, e.g. x==10, are guards; blue statements, e.g. y=0, are assignments; purple expressions, e.g. x<=60, are invariants of locations; purple names, e.g. red, are names of locations; communication channels are light blue, e.g. press?. The double-circled locations are the initial states.

There are two different clocks x and y; moreover the automata make use of the three synchronization channels press, syn and go. Every time unit corresponds to a second.

(a) Use English to describe each automaton separately.

For the remaining questions we consider the full (synchronised) system.

If you are asked to modify the system, only the parts that are changed need to be shown.

(b) As discussed in the lecture, a location of a timed automaton is a deadlock state if there are no (enabled) outgoing action-transitions. Does the system contain a deadlock? If yes, describe the situation when a deadlock can occur and modify the system such that no deadlocks can occur.

(c) Formalise the following properties in CTL, TCTL, or TCTLc. You can use the names of locations if you like to characterise that the system is in a particular location; you can also use properties on clocks such as x>42.

i. At no time pedestrians walk (across the street) while cars have green lights.

ii. The yellow light is never turned on for more than 10 seconds.

iii. After pressing the button a pedestrian is able to walk across the street within

40 seconds.

(d) Which of the properties in (c) hold for the deadlock-free system; which do not hold. Justify your answers.

(e) Modify the system in a way that all properties of (c) are valid.

(f) Extend the model by a “pedestrian cheat”: If a user presses the button three times within 3 seconds the system switches to a state where cars have to stop (state red) and pedestrians can walk.