CTL vs.
LTL
Robert Bellarmine Krug
Department of Computer Sciences
University of Texas at Austin
May 25, 2010
Outline
1. Some Definitions And Notation
2. LTL
3. CTL
4. CTL vs. LTL
CTL vs. LTL (2 / 40)
Outline
1. Some Definitions And Notation
2. LTL
3. CTL
4. CTL vs. LTL
CTL vs. LTL Some Definitions And Notation (3 / 40)
Kripke Structures — Definition
Let AP be a set of labels — i.e., a set of atomic propositions such
as Boolean expressions over variables, constants, and predicate
symbols.
A Kripke structure is a 4-tuple, M = (S, I , R, L):
I a finite set of states, S,
I a set of initial states, I ⊆ S,
I a transition relation, R ⊆ S × S where
∀s ∈ S, ∃s 0 ∈ S such that (s, s 0 ) ∈ R,
I a labeling function, L, from states to the power set of atomic
propositions, L : S → 2AP .
CTL vs. LTL Some Definitions And Notation (4 / 40)
Kripke Structure — An Example
S = {s0 , s1 , s2 , s3 }
I = {s0 }
R = {{s0 , s1 } s_0 s_1
{s0 , s2 }
{s1 , s1 } p p, q
{s1 , s3 }
{s2 , s0 }
{s2 , s3 }
{s3 , s0 }}
p, r v
L = {{s0 , {p}}
{s1 , {p, q}} s_2 s_3
{s2 , {p, r }}
{s3 , {v }}}
CTL vs. LTL Some Definitions And Notation (5 / 40)
Infinite Paths
LTL and CTL are concerned only with infinite paths. From here
on, π will always denote an infinite path. Furthermore, π0 will
always denote π’s first element, π1 its second element, and so on.
π = (π0 , π1 , π2 , . . .) is an infinite path in M if it respects M’s
transition relation, i.e., ∀i, (πi , πi+1 ) ∈ R.
π i denotes π’s ith suffix, i.e., π i = (πi , πi+1 , πi+2 , . . .)
(π i )j = (πi , πi+1 , πi+2 , . . .)j = (πi+j , πi+j+1 , πi+j+2 , . . .) = π i+j
CTL vs. LTL Some Definitions And Notation (6 / 40)
Outline
1. Some Definitions And Notation
2. LTL
3. CTL
4. CTL vs. LTL
CTL vs. LTL LTL (7 / 40)
LTL BNF Syntax
A well-formed LTL formula, φ, is recursively defined by the BNF
formula:
φ ::= > ; top, or true
| ⊥ ; bottom, or false
| p ; p ranges over AP
| ¬φ ; negation
| φ∧φ ; conjunction
| φ∨φ ; disjunction
| Xφ ; next time
| Fφ ; eventually
| Gφ ; always
| φUφ ; until
From here on, lowercase letters such as p, q, and r , will denote
atomic propositions. Greek letters such as φ and ψ will denote
formulae.
CTL vs. LTL LTL (8 / 40)
LTL Semantics — the Basics
We now define the binary satisfaction relation, denoted by , for
LTL formulae. This satisfaction is with respect a pair — hM, πi, a
Kripke structure and a path thereof.
First, the basics:
I M, π >
true is always satisfied
I M, π 6 ⊥
false is never satisfied
I (M, π p) if and only if (p ∈ L(π0 ))
atomic propositions are satisfied when they are members of
the path’s first element’s labels
CTL vs. LTL LTL (9 / 40)
LTL Semantics — Boolean Combinations
The use of the Boolean operators ¬, ∧, and ∨ in LTL formulae is a
deliberate pun on their mathematical meanings.
I (M, π ¬φ) if and only if (M, π 6 φ)
I (M, π φ ∧ ψ) if and only if [(M, π φ) ∧ (M, π ψ)]
I (M, π φ ∨ ψ) if and only if [(M, π φ) ∨ (M, π ψ)]
CTL vs. LTL LTL (10 / 40)
LTL Semantics — Temporal Operators
I (M, π X φ) if and only if (M, π 1 φ)
next time φ
I (M, π F φ) if and only if (∃i such that M, π i φ)
eventually φ
I (M, π G φ) if and only if (∀i such that M, π i φ)
always φ
I (M, π φUψ) if and only if
[ ∃i such that (∀j < i(M, π j φ)) ∧ (M, π i ψ)]
φ until ψ
N.B., The U used here is the “strong until.” There is also a “weak
until,” φUw ψ is equivalent to (φUψ) ∨ (G φ).
CTL vs. LTL LTL (11 / 40)
Xp — Example Path
M, (π0 , π1 , . . .) Xp
π π
0 1
CTL vs. LTL LTL (12 / 40)
Fp — Example Path
M, (π0 , π1 , π2 , π3 , . . .) Fp
π0 π1
π2 π3
CTL vs. LTL LTL (13 / 40)
Gp — Example Path
M, (π0 , π1 , π2 , π3 , . . .) Gp
p p
π0 π1
p p
π2 π3
CTL vs. LTL LTL (14 / 40)
pUq — Example Path
M, (π0 , π1 , π2 , π3 , . . .) pUq
p p
π0 π1
p q
π2 π3
CTL vs. LTL LTL (15 / 40)
pUq — Another Example Path
M, (π0 , . . .) pUq
π0
CTL vs. LTL LTL (16 / 40)
More LTL Semantics
I (M M φ) if and only if ∀π such that π0 ∈ I , (M, π φ)
A model, or Kripke structure, satisfies an LTL formula, when
all its paths do.
I (φ ≡ ψ) if and only if ∀M [(M M φ) ⇔ (M M ψ)]
Two LTL formulae are equivalent when they are satisfied by
the same Kripke structures.
CTL vs. LTL LTL (17 / 40)
An LTL Equivalence
X (φ ∧ ψ) ≡ X φ ∧ X ψ
By the previous slide, this is true if, for all M and π:
[M, π X (φ ∧ ψ)] ⇔ [M, π (X φ ∧ X ψ)]
[M, π X (φ ∧ ψ)] =
[M, π 1 (φ ∧ ψ)] = by definition of X
[(M, π 1 φ) ∧ (M, π 1 ψ)] = by definition of ∧
[(M, π X φ) ∧ (M, π X ψ)] = by definition of X
[M, π (X φ ∧ X ψ)] by definition of ∧
CTL vs. LTL LTL (18 / 40)
Some More LTL Equivalences
X (φ ∧ ψ) ≡ X φ ∧ X ψ
X (φ ∨ ψ) ≡ X φ ∨ X ψ
X (φUψ) ≡ (X φUX ψ)
¬X φ ≡ X ¬φ
F (φ ∨ ψ) ≡ F φ ∨ F ψ
G (φ ∧ ψ) ≡ G φ ∧ G ψ
¬F φ ≡ G ¬φ
(φ ∧ ψ)Uρ ≡ (φUρ) ∧ (ψUρ)
ρU(φ ∨ ψ) ≡ (ρUφ) ∨ (ρUψ)
FF φ ≡ F φ
GG φ ≡ G φ
CTL vs. LTL LTL (19 / 40)
