The University of New South Wales
COMP3153/9153
Algorithmic Verification
Final Take-Home Exam
Term 2, 2023
Time Allowed: 24 Hours
Total Number of Questions: 8
Total Number of Pages: 6 (including this title page)
Total Marks Available: 100
Answer all questions. The questions are not of equal value.
Produce a PDF file, either via LATEX or otherwise, with your prose answers.
Diagrams may be hand-drawn and can be included in the pdf or zipped together with the
pdf.
Submit with give cs3153 exam exam.pdf/exam.zip or with the give web interface.
Include the following statement in your PDF file:
I declare that all of the work submitted for this exam is my own work, completed
without assistance from anyone else.
You must adhere to the UNSW student conduct requirements listed at
https://student.unsw.edu.au/conduct.
Question 1 (10 marks)
Consider the following automaton C:
q0
L(q0) = {p}
q1
L(q1) = {p, q}
q2
L(q2) = {q}
q3
L(q3) = {p, q}
q4
L(q4) = {p, r}
q5
L(q5) = {p, r}
For each of the following CTL∗ formulae, determine whether C satisfies it or not.
Justify your answers.
(a) (F q)→ (G p)
(b) (FG p)→ (GF q)
(c) E(G (F¬p))
(d) AG (p→ AX q)
(e) G ((X q) ∨ (pU r))
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.
(c) Give an ACTL formula, φ, that holds in one of A or C and does not hold in the
other.
(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.
Page 2
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 = (F p)U q and φ2 = (F p) ∧ (F q)
(c) φ1 = AXE(pU q) and φ2 = E(pU (AX q)) ∨ q
(d) φ1 = X (pU (G q)) and φ2 = G ((X p)U (G q))
(e) φ1 = (X p)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.
(c) Prove the following:
i. ((pBefore q) ∧ q) implies p;
ii. pBefore (q ∨ r) is equivalent to ((pBefore q) ∧ (pBefore r)).
(d) Give a Bu¨chi automaton that accepts the words described by the formula pBefore 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.
Page 3
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, x
′
0, x
′
1):
x0
x1
x′0
x′1
•
•
• •
• •
0 1
Here a solid line indicates the Boolean value true, and a dashed line the value
false.
T (x0, x1, x
′
0, x
′
1) 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;
);
Page 4
(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.
(c) Compute the result of the live variable analysis, using backwards may analysis.
Question 7 (10 marks)
Consider the LTL formula:
φ = G (pU q)
Let Σ = 2{p,q} = {∅, {p}, {q}, {p, q}}
(a) Give a Bu¨chi automaton that accepts the words (in Σω) described by φ. Justify
your construction.
(b) Give a Bu¨chi automaton that accepts the words (in Σω) described by ¬φ. Justify
your construction.
(c) Give a safety property Ps and a liveness 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.
red
x<=60
yellow
green
x == 10
go!
x=0
syn?
x=0
(a) Traffic Lights for Cars
walk walk_granted
walk_requested
y<=30
stop
y>=30
go?
y=0
syn!
press?
y=0
press?
y=0
(b) Traffic Lights for Pedestrian
press!
(c) A User
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.
Page 5
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.
Don’t forget to submit your work and to include the statement listed on the front page.
END OF EXAM
Page 6