Model Checking and

Computation Tree
Logic (CTL)

-Kamrul Hasan Talukder

Professor
Computer Science and Engineering
Discipline
Khulna University, Bangladesh.
Correctness of Systems
• Verifying correctness of systems

• Testing
• Testing systems with test cases

• Formal methods
• Proof of correctness, e.g., theorem proving, model
checking

ICMCTI-2017, The University of

2
Burdwan
Formal Methods

• Given a system model and a property.

• Does the system satisfy the property?

• Verifying the correctness of the system

specified as properties

ICMCTI-2017, The University of

3
Burdwan
Model Checking

Property  System Model

Model Checker

Yes No, Counter example

ICMCTI-2017, The University of

4
Burdwan
System Model
• System modeled as labeled transition
system
• Kripke structures
• Graphs
• Vertices labeled by atomic proposition
• Edges represent transitions between states

ICMCTI-2017, The University of

5
Burdwan
Model Checking

Property  System Model

Temporal Logic Kripke Structure

Model Checker

Yes No, Counter example

ICMCTI-2017, The University of

6
Burdwan
Specification Language
• Specification language to specify
properties
• Temporal logic: formulas specify temporal
behaviors of a systems
• Examples of temporal logic
• Computation Tree Logic (CTL)
• Linear Temporal Logic (LTL)

ICMCTI-2017, The University of

7
Burdwan
System and Properties
• System modeled as Kripke structures
• Labeled transition systems

• Properties as temporal logic formulas

• Linear time: Linear time logic (LTL)
• Branching time: Computation Tree Logic
(CTL)

ICMCTI-2017, The University of

8
Burdwan
The Verification
Framework
• Start with a finite state transition system
TS = (S, s0, R)
• S is the set of states
• s0S is the set of initial states
• R  S  S is the transition relation.
• Identify a finite of atomic propositions AP.
• AP = {p, q, r, …}
• p = “The alarm light is on”
• q = “User 12 is waiting”
• r = “The buffer is full”

ICMCTI-2017, The University of

9
Burdwan
The Verification
Framework
• TS = (S, S0, R)
• AP = {p, q, r,..}
• L : S → 2AP
• Valuation function
• Specifies the (subset of ) atomic propositions that
are “True” at a state.
• Identifying AP and L is a part of the
modeling process.

ICMCTI-2017, The University of

10
Burdwan
Atomic Propositions
Req-1
PR1
Grt-1
Arbiter
Req-2 Resource
PR2
Grt-2

i1 – Process 1 is idle
w1– Process 1 is waiting
u1 – Process 1 is using the resource.
AP = { i1, w1, u1, i2, w2, u2}
ICMCTI-2017, The University of
11
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

ICMCTI-2017, The University of

12
Burdwan
 L(so) = {i1, i2}

s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2
L(s2) ={i1,
L(s5) = u2}
{w1,w2}
ICMCTI-2017, The University of
13
Burdwan
 L(so) = {i1, i2}

s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

L(s3) = {w1, i2
}
ICMCTI-2017, The University of
14
Burdwan
Computation Tree Logic
• TS = (S, S0, R)
• AP = {p, q, r,..}
• L : S → 2AP
• K = (S, S0, R, AP, L) is called a Kripke structure.
• Using AP, build a CTL formula .
• Ask K, s ╞  ?
• Is  true in K at s?
• This is the CTL model checking problem !

ICMCTI-2017, The University of

15
Burdwan
CTL
• Syntax
• AP – a finite set of atomic propositions.
• p  AP is a formula.
• If y and y’ are formulas then so are
• y
• y  y’.
• If y is a formula then so is EX(y)
• If y is a formula then so are
• EF(y)
• AF(y).

ICMCTI-2017, The University of

16
Burdwan
Computation Tree Logic (CTL)
• In CTL we quantify over the paths in the
computation tree
• We use the same four temporal operators: X,
G, F, U
• However we attach path quantifiers to these
temporal operators:
• A : for all paths
• E : there exists a path
• We end up with eight temporal operators:
• AX, EX, AG, EG, AF, EF, AU, EU

ICMCTI-2017, The University of

17
Burdwan
CTL Semantics
• Given a state s and CTL properties p and q
• s |= p iff L(s, p) = True, where p  AP
• s |= p iff not s |= p
• s |= p  q iff s |= p and s |= q
• s |= p  q iff s |= p or s |= q
• s0 |= EX p iff there exists a path s0, s1, s2, ...
such that s1 |= p
• s0 |= AX p iff for all paths s0, s1, s2, ..., s1 |=
p

ICMCTI-2017, The University of

18
Burdwan
CTL Semantics
• s0 |= EG p iff there exists a path s0, s1, s2, ... such
that for all i  0, si |= p
• s0 |= AG p iff for all paths s0, s1, s2, ..., for all i  0,
si |= p
• s0 |= EF p iff there exists a path s0, s1, s2, ... such
that there exists an i  0 such that si |= p
• s0 |= AF p iff for all paths s0, s1, s2, ..., there exists
an i  0, such that, si |= p
• s0 |= p EU q iff there exists a path s0, s1, s2, ...,
such that, there exists an i  0 such that si |= q and
for all 0  j < i, sj |= p
• s0 |= p AU q iff for all paths s0, s1, s2, ..., there
exists an i0 such that si|=q and for all 0 j< i, sj|=p

ICMCTI-2017, The University of

19
Burdwan
CTL Equivalences

• AX p =  EX p
• AG p =  EF p
• AF p =  EG p
• p AU q = ( (q EU (p q))  EG  q)
• EF p = True EU p

ICMCTI-2017, The University of

20
Burdwan
 Formulas
 EX(p  EF(AF( p  r)))
EX


p EF
AF

 r

p
ICMCTI-2017, The University of
21
Burdwan
Semantics
• K = (S, S0, R, AP, L)
• L : S → 2AP
• y a CTL- formula sS
• K, s ╞ y
• y (holds) is satisfied at s.

ICMCTI-2017, The University of

22
Burdwan
Semantics
• CTL ::= p | y | y1  y2 | EX(y) |
EF(y) | AF(y)
• K = (S, S0, R, AP, L); L: → 2AP s  S
• K, s ╞ p iff p  L(s).
• K, s ╞  y iff it is NOT the case K, s ╞ y
• K, s ╞ y1  y2 iff
• K, s ╞ y1 OR K, s ╞ y2.

ICMCTI-2017, The University of

23
Burdwan
 s0
Req1 Req2
Ret2
Ret s3 s1
1 Grt1 Grt2
Req Req
2 1
s4 Ret s5 Ret2 s2
1 Grt2
Req2 Grt1 Req1
L(s2) ={i1,
L(s5) = u2}
{w1,w2} K, s5 ╞ w1 True
K, s0 ╞ w2 False
ICMCTI-2017, The University of
24
Burdwan
 s0
Req1 Req2
Ret2
Ret s3 s1
1 Grt1 Grt2
Req Req
2 1
s4 Ret s5 Ret2 s2
1 Grt2
Req2 Grt1 Req1
L(s2) ={i1,
L(s5) = u2}
{w1,w2}K, s5 ╞  i1 True

K, s0 ╞ w2  i1 True
ICMCTI-2017, The University of
25
Burdwan
 s0
Req1 Req2
Ret2
Ret s3 s1
1 Grt1 Grt2
Req Req
2 1
s4 Ret s5 Ret2 s2
1 Grt2
Req2 Grt1 Req1
L(s2) ={i1,
L(s5) = u2}
{w1,w2}K, s5 ╞  i1 True

K, s1 ╞  i1  u2 False
ICMCTI-2017, The University of
26
Burdwan
Semantics
• K = (S, S0, R, AP, L); L: → 2AP s  S
• K, s ╞ EX(y) there exists s’ such that:
• s → s’ (R(s, s’)) and
• K, s’ ╞ y
• s has a successor state s’ at which y holds.

ICMCTI-2017, The University of

27
Burdwan
 off
S0 AP = {B, G, R}
off on on

S1 S2

K, S0 ╞ EX(R) true
K, S0 ╞ EX(R) true
K, S1 ╞ EX(R) true
K, S2 ╞ EX(G) false

ICMCTI-2017, The University of

28
Burdwan
Semantics
• K = (S, S0, R, AP, L); L: → 2AP s  S
• A path from s is a sequence of states p =
s0, s1, s2, …,si, si+1, … such that:
• s = s0
• si → si+1 (R(si, si+1)) for every i.
• p(i) = si the i th element of p.
• Assume for convenience that for every s
there is s’ such that R(s, s’).

ICMCTI-2017, The University of

29
Burdwan
Semantics
• CTL ::= p | y | y1  y2 | EX(y) |
EF(y) | AF(y)
• K = (S, S0, R, AP, L); L: → 2AP
sS
• K, s ╞ EF(y) iff there exists a
path p = s0, s1, … from s and k
 0 such that: K, p(k) ╞ y
ICMCTI-2017, The University of
30
Burdwan
 s ╞ EF(

s1

sj

sk ╞ 

ICMCTI-2017, The University of

31
Burdwan
Semantics
• CTL ::= p | y | y1  y2 | EX(y) |
EF(y) | AF(y)
• K = (S, S0, R, AP, L); L: → 2AP s  S
• K, s ╞ AF(y) iff for every path p = s0, s1,
… from s there exists k  0 such that: K,
p(k) ╞ y

ICMCTI-2017, The University of

32
Burdwan
 AF()








ICMCTI-2017, The University of

33
Burdwan
 0
Req2

3
Req Grt2
1
5
Grt 4
1 Ret
7 1
0

K, 0 ╞ AF(u1) false

ICMCTI-2017, The University of

34
Burdwan
 0
Req2

3
Req Grt2
1
5
Grt 4
1 Ret
7 1
0

K, 0 ╞ AF(EF(u1)) True

ICMCTI-2017, The University of

35
Burdwan
Derived Operator
• AX(y) = EX(y)
• It is not the case there exists a next state at
which y does not hold.
• For every next state y holds.

AX(y)

y y
y

ICMCTI-2017, The University of

36
Burdwan
Derived Operators
• K, s ╞ AG(y)
• AG(y) = EF(y)
• It is not the case there exists a path p (from
s) and k  0 such that:
• K, p(k) ╞ y
• For every path p (from s) and every k:
• K, p(k) ╞ y

ICMCTI-2017, The University of

37
Burdwan
 AG()








ICMCTI-2017, The University of

38
Burdwan
Derived Operators
• K, s ╞ EG(y)
• EG(y) = AF(y)
• It is not the case that for every path p from s
there is a k  0 such that K, p(k) ╞ y.
• There exists a path p from s such that, for
every k  0:
• K, p(k) ╞ y.

ICMCTI-2017, The University of

39
Burdwan
 EG()

ICMCTI-2017, The University of

40
Burdwan
CTL- Model Checking
• The actual model checking problem:
• Given K = (S, S0, R, AP, L)
• Given sS
• Given y, a CTL formula.
• Determine:
• K, s ╞ y

ICMCTI-2017, The University of

41
Burdwan
 L(so) = {i1, i2}

s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2
L(s2) ={i1,
L(s5) = u2}
K, s0 ╞ AX(w1) false
{w1,w2}
ICMCTI-2017, The University of
42
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ AX(w1  w2)
ICMCTI-2017, The University of
true Burdwan
43
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ EF(u2) true
ICMCTI-2017, The University of
44
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ EF(u1  u2) u1  u2 =  ( u1   u2) False

ICMCTI-2017, The University of
45
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ AG(u1  u2) false

ICMCTI-2017, The University of
46
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ AG( (u1  u2)) true

ICMCTI-2017, The University of
47
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ EG( u2) true

ICMCTI-2017, The University of
48
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ AF( u2) false

ICMCTI-2017, The University of
49
Burdwan
 s0
Req1 Req2
Ret2
Ret1 s3 s1
Grt1 Req2 Grt2
Req1

s4 Ret1 s5 Ret2 s2
Grt2
Req Grt1 Req1
2

K, s0 ╞ AF(u1  u2 )
ICMCTI-2017, The University of
true Burdwan
50
CTL Properties
Transition System Computation Tree
s3 p
p p
s1 s2 s3 s4
s4 p s1

s3 p s2
s3 |= p s3 |= EX p
s4 |= p s3 |= EX  p p s4 s1 s3 p
s1 |= p s3 |=  AX p ..
..
..
.
.
.
s2 |= p s3 |=  AX  p p s4 s1
. .
.
.
.
.
s3 |= EG p . . .

s3 |=  EG  p
s3 |= AF p
s3 |= EF  p
s3 |=  AF 
ICMCTI-2017, Thep
University of
51
Burdwan
CTL Model Checking
• The actual model checking problem:
• Given K = (S, S0, R, AP, L)
• Given s  S
• Given y, a CTL formula.
• Determine:
• K, s ╞ y
• This can be done “efficiently”
• Can be automated:
• Symbolic Model Verifier (SMV)

ICMCTI-2017, The University of

52
Burdwan
L (1) = {~heat, ~start, ~close,
~error}
L (2) = {~heat, start, ~close, 1
error} open
L (3) = {~heat, ~start, close, start door
~error} oven cook
open door
L (4) = {heat, ~start, close, close
~error} door
L (5) = {~heat, start, close, done
2 3 4
error}
L (6) = {~heat, start, close,
Verify: close
~error}
AG (start  AF heat) door start
L For
(7) simplicity
= {heat, start, close, open start
cooki
door oven
~error}.
~EF (start  EG ~heat). ng
State (start) = {2, 5, 6, 7}. rese
State (~heat) = {1, 2, 3, 5, 6}. t warmup
For EG ~heat, discard those 5 6 7
states from this where EG ~heat
does not hold. Obviously, such Include those states from where there is at
state is only 6 least one path to enter either state 2 or 5 in order to
State (EG ~heat) = {1, 2, 3, 5}.compute State (EF (start  EG ~heat)).
State (start  EG ~heat) will beState (EF (start  EG ~heat)) = {1, 2, 3, 4, 5, 6, 7}
the intersection of State (start)State (~EF (start  EG ~heat)) = {}
and State (EG ~heat) As the initial state 1 is not included in State (~EF
(start  EG ~heat)), the system described by this
State (start  EG ~heat)
ICMCTI-2017, The University of
= {2, 5} Kripke Structure
Burdwan
does not satisfy this specification
53
Fairness Constraint
• In verifying systems, we are occasionally interested only in
correctness along fair execution
• It is often necessary to introduce some notion of fairness.
• If there are two processes trying to use a shared resource using an
arbiter, we may wish to consider only those executions in which the
arbiter does not ignore one of its request inputs from either of the
processors forever.
• We may want to consider communication protocols that operate
over reliable channels which have the property that no message is
ever continuously transmitted but never received.
• A fairness constraint can be an arbitrary set of states, usually
described by the formula of the logic.
• If fairness constraints are interpreted as a set of states, then a
fair path must contain an element of each constraint infinitely
often.
• If fairness constraints are interpreted as CTL formulas, then a
path is fair if each constraint is true infinitely often along the
path.
ICMCTI-2017, The University of
54
Burdwan
 Using Fairness
 We consider only the path along
which the user operates the
microwave oven correctly infinitely
often
 the formula start  close  ~error
holds infinitely often.
 Thus the fairness set F = {A}, where
A = {s| s |= start  close  ~error}.

ICMCTI-2017, The University of

55
Burdwan
 Using Fairness
In this case State (start) = {2, 5, 6, 7} and State (~h
{1, 2, 3, 5, 6}.
In these two sets, there is at
least one state where start  close  ~error hold

But the previously computed State (EG ~heat) = {1, 2

is not valid in this case as none of these states
start  close  ~error holds.

State (EG ~heat) = {}.

State (EF (start  EG ~heat)) = {}.
State (~EF (start  EG ~heat)) = {1, 2, 3, 4, 5, 6, 7}

ICMCTI-2017, The University of

56
Burdwan
Conclusion
• The model checking with CTL logic has been
presented here.
• Symbolic Model Verifier (SMV)
• SPIN

ICMCTI-2017, The University of

57
Burdwan
Thank you.

ICMCTI-2017, The University of

58
Burdwan