Safety Properties
Bad events never happen
deadlock: two processes waiting for input from each other,
the system is unable to perform a transition.
no reachable state satisfies a “bad” condition,
e.g. never two processes in critical section at the same time
Can be refuted by a finite behaviour
Ex.: it is never the case that p.
28 / 96
Safety Properties
Bad events never happen
deadlock: two processes waiting for input from each other,
the system is unable to perform a transition.
no reachable state satisfies a “bad” condition,
e.g. never two processes in critical section at the same time
Can be refuted by a finite behaviour
Ex.: it is never the case that p.
28 / 96
Safety Properties
Bad events never happen
deadlock: two processes waiting for input from each other,
the system is unable to perform a transition.
no reachable state satisfies a “bad” condition,
e.g. never two processes in critical section at the same time
Can be refuted by a finite behaviour
Ex.: it is never the case that p.
28 / 96
Liveness Properties
Something desirable will eventually happen
sooner or later this will happen
Can be refuted by infinite behaviour
an infinite behaviour can be typically presented as a loop
29 / 96
Liveness Properties
Something desirable will eventually happen
sooner or later this will happen
Can be refuted by infinite behaviour
−p
−p −p −p
−p
−p −p
−p
an infinite behaviour can be typically presented as a loop
29 / 96
Liveness Properties
Something desirable will eventually happen
sooner or later this will happen
Can be refuted by infinite behaviour
−p
−p −p −p
−p
−p −p
−p
an infinite behaviour can be typically presented as a loop
29 / 96
Fairness Properties
Something desirable will happen infinitely often
important subcase of liveness
whenever a subroutine takes control, it will always return it (sooner or later)
Can be refuted by infinite behaviour
a subroutine takes control and never returns it
an infinite behaviour can be typically presented as a loop
30 / 96
Fairness Properties
Something desirable will happen infinitely often
important subcase of liveness
whenever a subroutine takes control, it will always return it (sooner or later)
Can be refuted by infinite behaviour
a subroutine takes control and never returns it
p p
p p
p p
p p
an infinite behaviour can be typically presented as a loop
30 / 96
Computation tree vs. computation paths
Consider the following Kripke structure:
!done done
Its execution can be seen as:
32 / 96
Computation tree vs. computation paths
Consider the following Kripke structure:
!done done
Its execution can be seen as:
32 / 96
Computation tree vs. computation paths
Consider the following Kripke structure:
!done done
Its execution can be seen as:
an infinite set of an infinite
computation paths computation tree
!done !done !done !done
!done !done !done done
.....
!done !done done done
!done done done done
32 / 96
Computation tree vs. computation paths
Consider the following Kripke structure:
!done done
Its execution can be seen as:
an infinite set of an infinite
computation paths computation tree
!done !done !done !done !done
!done !done !done done !done done
.....
!done !done done done !done done done
!done done done done !done done done done
32 / 96
Temporal Logics
Express properties of “Reactive Systems”
nonterminating behaviours,
without explicit reference to time.
Linear Temporal Logic (LTL)
interpreted over each path of the Kripke structure
linear model of time
temporal operators
“Medieval”: “since birth, one’s destiny is set”.
Computation Tree Logic (CTL)
interpreted over computation tree of Kripke model
branching model of time
temporal operators plus path quantifiers
“Humanistic”: “one makes his/her own destiny step-by-step”.
33 / 96
Temporal Logics
Express properties of “Reactive Systems”
nonterminating behaviours,
without explicit reference to time.
Linear Temporal Logic (LTL)
interpreted over each path of the Kripke structure
linear model of time
temporal operators
“Medieval”: “since birth, one’s destiny is set”.
Computation Tree Logic (CTL)
interpreted over computation tree of Kripke model
branching model of time
temporal operators plus path quantifiers
“Humanistic”: “one makes his/her own destiny step-by-step”.
33 / 96
Temporal Logics
Express properties of “Reactive Systems”
nonterminating behaviours,
without explicit reference to time.
Linear Temporal Logic (LTL)
interpreted over each path of the Kripke structure
linear model of time
temporal operators
“Medieval”: “since birth, one’s destiny is set”.
Computation Tree Logic (CTL)
interpreted over computation tree of Kripke model
branching model of time
temporal operators plus path quantifiers
“Humanistic”: “one makes his/her own destiny step-by-step”.
33 / 96
Linear Temporal Logic (LTL): Syntax
An atomic proposition is a LTL formula;
if ϕ1 and ϕ2 are LTL formulae, then ¬ϕ1, ϕ1 ∧ ϕ2, ϕ1 ∨ ϕ2, ϕ1 → ϕ2, ϕ1 ↔ ϕ2, ϕ1 ⊕ϕ2 are
LTL formulae;
if ϕ1 and ϕ2 are LTL formulae, then Xϕ1, Gϕ1, Fϕ1, ϕ1Uϕ2 are LTL formulae, where X, G, F,
U are the “next”, “globally”, “eventually”,“until” temporal operators respectively.
Another operator R “releases” (the dual of U) is used sometimes.
36 / 96
Linear Temporal Logic (LTL): Syntax
An atomic proposition is a LTL formula;
if ϕ1 and ϕ2 are LTL formulae, then ¬ϕ1, ϕ1 ∧ ϕ2, ϕ1 ∨ ϕ2, ϕ1 → ϕ2, ϕ1 ↔ ϕ2, ϕ1 ⊕ϕ2 are
LTL formulae;
if ϕ1 and ϕ2 are LTL formulae, then Xϕ1, Gϕ1, Fϕ1, ϕ1Uϕ2 are LTL formulae, where X, G, F,
U are the “next”, “globally”, “eventually”,“until” temporal operators respectively.
Another operator R “releases” (the dual of U) is used sometimes.
36 / 96
Linear Temporal Logic (LTL): Syntax
An atomic proposition is a LTL formula;
if ϕ1 and ϕ2 are LTL formulae, then ¬ϕ1, ϕ1 ∧ ϕ2, ϕ1 ∨ ϕ2, ϕ1 → ϕ2, ϕ1 ↔ ϕ2, ϕ1 ⊕ϕ2 are
LTL formulae;
if ϕ1 and ϕ2 are LTL formulae, then Xϕ1, Gϕ1, Fϕ1, ϕ1Uϕ2 are LTL formulae, where X, G, F,
U are the “next”, “globally”, “eventually”,“until” temporal operators respectively.
Another operator R “releases” (the dual of U) is used sometimes.
36 / 96
Linear Temporal Logic (LTL): Syntax
An atomic proposition is a LTL formula;
if ϕ1 and ϕ2 are LTL formulae, then ¬ϕ1, ϕ1 ∧ ϕ2, ϕ1 ∨ ϕ2, ϕ1 → ϕ2, ϕ1 ↔ ϕ2, ϕ1 ⊕ϕ2 are
LTL formulae;
if ϕ1 and ϕ2 are LTL formulae, then Xϕ1, Gϕ1, Fϕ1, ϕ1Uϕ2 are LTL formulae, where X, G, F,
U are the “next”, “globally”, “eventually”,“until” temporal operators respectively.
Another operator R “releases” (the dual of U) is used sometimes.
36 / 96
LTL semantics: intuitions
LTL is given by the standard boolean logic enhanced with the following temporal operators,
which operate through paths ⟨s0, s1, ..., sk , ...⟩:
“Next” X: Xϕ is true in st iff ϕ is true in st +1
“Finally” (or “eventually”) F: Fϕ is true in st iff ϕ is true in some st' with t ′ ≥ t
“Globally” (or “henceforth”) G: Gϕ is true in st iff ϕ is true in all st' with t ′ ≥ t
“Until” U: ϕUψ is true in st iff, for some state s t ' s.t t ′ ≥ t:
ψ is true in s t ' and
ϕ is true in all states st ' ' s.t. t ≤ t ′ ′ < t ′
“Releases” R: ϕRψ is true in st iff, for all states s t ' s.t. t ′ ≥ t:
ψ is true or
ϕ is true in some states st ' ' with t ≤ t ′ ′ < t ′
“ψ can become false only if ϕ becomes true first"
37 / 96
LTL semantics: intuitions
finally P globally P
FP GP
next P P until q
XP PUq
38 / 96
LTL: Some Noteworthy Examples
Safety: “it never happens that a train is arriving and the bar is up”
G(¬(train_arriving ∧ bar_up))
Liveness: “if input, then eventually output”
G(input → Foutput)
Releases: “the device is not working if you don’t first repair it”
(repair_device R ¬working_device)
Fairness: “infinitely often send ”
GFsend
Strong fairness: “infinitely often send implies infinitely often recv.”
GFsend → GFrecv
39 / 96
LTL Formal Semantics
π, si |= a iff a ∈ L(si )
π, si |= ¬ϕ iff π, si |= ϕ
π, si |= ϕ ∧ ψ iff π, si |= ϕ and
π, si |= ψ
π, si |= Xϕ iff π, si+1 |= ϕ
π, si |= Fϕ iff for some j ≥ i : π, sj |= ϕ
π, si |= Gϕ iff for all j ≥ i : π, sj |= ϕ
π, si |= ϕUψ iff for some j ≥ i : (π, sj |= ψ and
for all k s.t. i ≤ k < j : π, sk |= ϕ)
π, si |= ϕRψ iff for all j ≥ i : (π, sj |= ψ or
for some k s.t. i ≤ k < j : π, sk |= ϕ)
40 / 96
LTL Formal Semantics (cont.)
LTL properties are evaluated over paths, i.e., over infinite, linear sequences of states:
π = s0 → s1 → · · · → st → st +1 → · · ·
Given an infinite sequence π = s0 , s1 , s2 , . . .
π, si |= φ if φ is true in state si of π.
π |= φ if φ is true in the initial state s0 of π.
The LTL model checking problem M |= φ
check if π |= φ for every path π of the Kripke structure M (e.g., φ = Fdone)
41 / 96
LTL Formal Semantics (cont.)
LTL properties are evaluated over paths, i.e., over infinite, linear sequences of states:
π = s0 → s1 → · · · → st → st +1 → · · ·
Given an infinite sequence π = s0 , s1 , s2 , . . .
π, si |= φ if φ is true in state si of π.
π |= φ if φ is true in the initial state s0 of π.
The LTL model checking problem M |= φ
check if π |= φ for every path π of the Kripke structure M (e.g., φ = Fdone)
41 / 96
LTL Formal Semantics (cont.)
LTL properties are evaluated over paths, i.e., over infinite, linear sequences of states:
π = s0 → s1 → · · · → st → st +1 → · · ·
Given an infinite sequence π = s0 , s1 , s2 , . . .
π, si |= φ if φ is true in state si of π.
π |= φ if φ is true in the initial state s0 of π.
The LTL model checking problem M |= φ
check if π |= φ for every path π of the Kripke structure M (e.g., φ = Fdone)
!done !done !done !done
!done !done !done done
.....
!done !done done done
!done done done done
!done done
41 / 96
Syntactic properties of LTL operators
ϕ1 ∨ ϕ2 ⇐⇒ ¬(¬ϕ 1 ∧ ¬ϕ 2 )
...
F ϕ1 ⇐⇒ TUϕ 1
G ϕ1 ⇐⇒ ⊥Rϕ1
Fϕ1 ⇐⇒ ¬G¬ϕ 1
Gϕ1 ⇐⇒ ¬F¬ϕ 1
¬Xϕ1 ⇐⇒ X¬ϕ1
ϕ1Rϕ2 ⇐⇒ ¬(¬ϕ 1 U¬ϕ 2 )
ϕ1Uϕ2 ⇐⇒ ¬(¬ϕ 1 R¬ϕ 2 )
Note
LTL can be defined in terms of ∧, ¬, X, U only
Exercise
Prove that ϕ1Rϕ2 ⇐⇒ Gϕ2 ∨ ϕ2U(ϕ1 ∧ ϕ2)
44 / 96
Syntactic properties of LTL operators
ϕ1 ∨ ϕ2 ⇐⇒ ¬(¬ϕ 1 ∧ ¬ϕ 2 )
...
F ϕ1 ⇐⇒ TUϕ 1
G ϕ1 ⇐⇒ ⊥Rϕ1
Fϕ1 ⇐⇒ ¬G¬ϕ 1
Gϕ1 ⇐⇒ ¬F¬ϕ 1
¬Xϕ1 ⇐⇒ X¬ϕ1
ϕ1Rϕ2 ⇐⇒ ¬(¬ϕ 1 U¬ϕ 2 )
ϕ1Uϕ2 ⇐⇒ ¬(¬ϕ 1 R¬ϕ 2 )
Note
LTL can be defined in terms of ∧, ¬, X, U only
Exercise
Prove that ϕ1Rϕ2 ⇐⇒ Gϕ2 ∨ ϕ2U(ϕ1 ∧ ϕ2)
44 / 96
Example 1: mutual exclusion (safety)
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= G¬(C1 ∧ C2 ) ?
50 / 96
Example 1: mutual exclusion (safety)
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= G¬(C1 ∧ C2 ) ?
YES: There is no reachable state in which (C1 ∧ C2) holds!
50 / 96
Example 2: liveness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= FC1 ?
51 / 96
Example 2: liveness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= FC1 ?
NO: there is an infinite cyclic solution in which C1 never holds!
51 / 96
Example 3: liveness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= G(T1 → FC1 ) ?
52 / 96
Example 3: liveness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= G(T1 → FC1 ) ?
YES: every path starting from each state where T1 holds passes through a state where C1 holds.
52 / 96
Example 4: fairness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= GFC1 ?
53 / 96
Example 4: fairness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= GFC1 ?
NO: e.g., in the initial state, there is an infinite cyclic solution in which C1 never holds!
53 / 96
Example 5: strong fairness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= GFT1 → GFC1 ?
54 / 96
Example 5: strong fairness
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= GFT1 → GFC1 ?
YES: every path which visits T1 infinitely often also visits C1 infinitely often
(see liveness property of previous example).
54 / 96
Example 6: blocking
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= G(N1 → F T1 ) ?
55 / 96
Example 6: blocking
N = noncritical, T = trying, C = critical N1, N2 User 1 User 2
turn=0
T1, N2 N1, T2
turn=1 turn=2
C1, N2 T1, T2 T1, T2 N1, C2
turn=1 turn=1 turn=2 turn=2
C1, T2 T1, C2
turn=1 turn=2
M |= G(N1 → F T1 ) ?
NO: e.g., in the initial state, there is an infinite cyclic solution in which N1 holds and T1 never
holds!
55 / 96
