COMP2620/6262 (Logic) Tutorial

Week 11
Semester 1, 2026

Tutorial Test
In each tutorial, apart from week 2, there is a short test on skills practised in the previous tutorial. Your
top 8 test attempts, out of the 10 available, will collectively count for 50% of your final mark.
This week’s test is on modelling English into CTL*. Your tutor will hand out blank paper, on
which you should clearly write your university ID and name. Your tutor will also hand out paper with
an English language description of current and future states of a situation. You will translate each line
of the description into a CTL* proposition. You must use CTL* syntax - not LTL or CTL, even if you
feel that an LTL or CTL proposition could be used. Where you believe the English language description
is ambiguous, you will be asked to present what you think is the most plausible translation, and then
briefly discuss what other translations might be reasonable. You will have eight minutes to do this.
You are not permitted to have any other resource on the table during this test, including any electronic
device. If you finish your test before time elapses you may put your hand up and your tutor will collect
your sheet. Once you have done this, you may get a device out and start work silently on this week’s
questions. If you are still working when time elapses you must stop writing immediately and let your
tutor collect your paper.

This Week’s Exercises

This week we will perform CTL model checking:
ˆ Label each state with propositional variables according to the labelling function
ˆ Label nothing with ⊥
ˆ If a state is not labelled with φ, label it with ¬φ
ˆ If a state is labelled with both φ and ψ, label it with φ ∧ ψ
ˆ If a state is labelled with either φ or ψ, or both, label it with φ ∨ ψ
ˆ Label a state with EXφ if any of its successors are labelled with φ
ˆ Label with E[φ U ψ] all states that are labelled with ψ, then label with E[φ U ψ] all states that are
labelled with φ for which some immediate successor is labelled with E[φ U ψ], until done
ˆ Label with EGφ all states that are labelled with φ, then delete EGφ from any state with no
successors labelled with EGφ, until done, or
ˆ Label with EGφ any state in the subgraph of states labelled φ that can reach a non-trivial SCC
in any number of transitions

We will also perform LTL model checking.

First step: defining our states
ˆ States get variable labels according the labelling function.
ˆ No state gets label ⊥.
ˆ If a state is not labelled with φ, label it with ¬φ

1
 ˆ If a state is labelled with both φ and ψ, label it with φ ∧ ψ

ˆ If a state is labelled with either φ or ψ, or both, label it with φ ∨ ψ

ˆ Make copies of each state with and without Xφ

ˆ If a state has ψ, label it with φ U ψ. If a state has φ but not does not have ψ, make copies with
and without φ U ψ.
Second step: adding transitions. Given states s′ , t′ , which are copies of s, t from the original system,
add a transition s′ → t′ if there was a transition s → t in the original system and

ˆ If s′ has Xφ then t′ must have φ

ˆ If s′ does not have Xφ then t′ must not have φ

ˆ If s′ has φ U ψ and does not have ψ, then t′ must have φ U ψ

ˆ If s′ has φ and does not have φ U ψ, then t′ must not have φ U ψ

Third step: pruning states. Until no more deletions are possible:

ˆ Delete any state without a transition out of it

ˆ Delete any state with φ U ψ that has no path to a state with ψ

1. The test at the start of the next tutorial will resemble this question.
Model check the following CTL propositions against the transition system below. You should label
all states with all correct subformulas of the target propositions.

s0 s1 s2
p p p, q

q q
s3 s4

ˆ EX(p ∧ EXq)
Solution. s0 : p, EXq, p ∧ EXq, EX(p ∧ EXq); s1 : p, EXq, p ∧ EXq, EX(p ∧ EXq);
s2 : p, q, EXq, p ∧ EXq; s3 : q, EXq; s4 : q, EXq, EX(p ∧ EXq).
ˆ E[p U ¬p ∧ EXp]
Solution. s0 : p, EXp, E[p U ¬p ∧ EXp]; s1 : p, EXp, E[p U ¬p ∧ EXp]; s2 : p, E[p U ¬p ∧
EXp]; s3 : ¬p; s4 : ¬p, EXp, ¬p ∧ EXp, E[p U ¬p ∧ EXp].
ˆ EG¬EG(p ∧ ¬q)
Solution. s0 : p, ¬q, p ∧ ¬q, EG(p ∧ ¬q); s1 : p, ¬q, p ∧ ¬q, ¬EG(p ∧ ¬q), EG¬EG(p ∧ ¬q);
s2 : p, q, ¬EG(p∧¬q), EG¬EG(p∧¬q); s3 : q, ¬EG(p∧¬q), EG¬EG(p∧¬q); s4 : q, ¬EG(p∧
¬q), EG¬EG(p ∧ ¬q).

Do likewise with the following transition system and CTL propositions.

q s1
s0

p p, q
s2 s3

2
 ˆ EXq ∨ EGp
Solution. s0 : EXq, EXq ∨ EGp; s1 : q, EXq, EXq ∨ EGp; s2 : p, EXq, EGp, EXq ∨ EGp;
s3 : p, q, EGp, EXq ∨ EGp.
ˆ E[EXp U EGq]
Solution. s0 : EXp, E[EXp U EGq]; s1 : q, EGq, E[EXp U EGq]; s2 : p, EXp; s3 :
p, q, EXp.

2. Identify the Strongly Connected Components (SCCs) in the transition systems above. Are any of
them trivial?
Solution. For the first system, s0 on its own is one SCC; all the other states together form the
only other SCC. Neither is trivial: although s0 forms an SCC on its own, it has a self loop.
For the second system there are three SCCs: s0 on its own, s1 on its own, and s2 and s3 together.
s0 on its own is the only trivial SCC.
If you did not do so already, solve the EGφ parts of each of the questions above using the more
efficient SCC method (if you did use that method, you could instead try out the simpler deletion-
based method).
Solution. For the SCC-based model check for EG(p ∧ ¬q) for the first system, we first consider
the subgraph of states that satisfy p ∧ ¬q:

s0 s1

s0 and s1 each form one element SCCs, but only the s1 one is trivial. So we label s0 with EG(p∧¬q)
and do not give this label to s1 , because it has no path to a non-trivial SCC.
For the model check for EG¬EG(p ∧ ¬q) we disregard s0 . Then the whole graph is a single SCC
so everything in that graph gets the label.
For the EGp case of the second system, we look only at s2 and s3 , and label both. For the EGq
case we look only at s1 and s3 . Then s1 is part of a non-trivial SCC so gets the label; s3 in this
subgraph is not part of a non-trivial SCC, and nor can it reach one, so it does not get the label.
3. This system models a priority process and a secondary process which both need access to some non-
shareable resource. Requests come in for these processes (rp , rs ) and they can do work (wp , ws ),
but the priority process takes precedence, with requests for it even making the secondary process
pause if it has started its work. We assume that after each process finishes work it must be inactive
for one step to check whether it has any pending requests.

wp

rp

wp , rs

rp , rs

ws , rp

rs

ws

ˆ State a CTL proposition that means that, if the secondary process starts work, it will even-
tually become inactive (neither working nor holding a pending request).
Solution. AG(ws → AF (¬ws ∧ ¬rs ))

3
 ˆ Give a reason (informally) that this proposition fails.
Solution. We can get stuck in a loop from ws , rp (the secondary process is working but a
priority request has been recieved) to wp , rs (the secondary process is paused to do the priority
work) to rs (the priority work is finished) then back to ws , rp (the secondary process restarts,
but another priority request is detected). We never reach a state satisfying ¬ws ∧ ¬rs . The
situation is the same if we sometimes include ws in our loop between rs and ws , rp .

4. Model check the following LTL propositions against the transition system below. You should label
all states in your expanded transition system. Clearly state whether the model check succeeds or
fails.

s t
p p, q

p
u v

ˆ p ∧ Xp
Solution. Initial graph with all possible states:
p, Xp, p ∧ Xp p, q, Xp, p ∧ Xp

p p, q

p, Xp, p ∧ Xp Xp

Erasing states without outbound transitions:

p, Xp, p ∧ Xp p, q, Xp, p ∧ Xp

p, q

Xp

Only one copy of the start state remains, and it satisfies p∧Xp, so the model check succeeds.
ˆ pU q
Solution. Initial graph (omitting for space reasons the p and q labels, which are as in the
original system):

4
 pU q

pU q

pU q

Only the bottom state gets deleted for lacking an outbound arrow. There remain two copies
of the start state, and one is not labelled p U q, so the model check fails.
ˆ GF p (You will need to convert this to use only the set of LTL connectives that we have learned
to model check: ⊥, ¬, ∧, ∨, X, U .)
Solution. GF p ≡ ¬F ¬F p ≡ ¬(⊤ U ¬(⊤ U p)). Initial graph, omitting ⊤ which is labelled
everywhere:

p,⊤ U p,⊤ U ¬(⊤ U p) p,⊤ U p,⊤ U ¬(⊤ U p)

p,⊤ U p,GF p p,⊤ U p,GF p

p,⊤ U p,GF p ⊤ U p,⊤ U ¬(⊤ U p)

⊤ U p,GF p
p,⊤ U p,⊤ U ¬(⊤ U p)

¬(⊤ U p),⊤ U ¬(⊤ U p)

We delete the bottom state because it has no outbound transitions. But then the entire
outside perimeter becomes useless, as all states claim ⊤ U ¬(⊤ U p) but no state in it delivers
on ¬(⊤ U p). So we delete those four states also, to end up with:

p,⊤ U p,GF p p,⊤ U p,GF p

p,⊤ U p,GF p ⊤ U p,GF p

Only one copy of the start state remains, and it satisfies GF p, so the model check succeeds.