Modal & temporal logic
Juraj Jurco
December 2, 2013
Masaryk University, Faculty of Informatics
adopted by Juraj Jurco from slides of Rajeev Gore
Kripke Semantics for Logical Consequence
Given some model W, R, ϑ and some w ∈ W, we compute the truth value of
a non-atomic formula by recursion on its shape:
ϑ(w, ϕ) =
t ϑ(v, ϕ) = t for some v ∈ W with wRv
f otherwise
ϑ(w, []ϕ) =
t ϑ(v, ϕ) = t for every v ∈ W with wRv
f otherwise
Example: If W = {w0, w1, w2} and R = {(w0, w1), (w0, w2)} and
ϑ(w1, p3) = t then W, R, ϑ is a Kripke model as pictured below:
w1
w0
R
##GGGGGGGG
R
;;wwwwwwww
w2
ϑ(w0, p3) = t
ϑ(w0, []p3) = f
ϑ(w1, []p1) = t
ϑ(w1, []¬p1) = t
ϑ(w0, []p1) = t
Intuition: truth of modalities depends on underlying R (not truth functional)
Introduction to Modal and Temporal Logics 6 December 2007 9
Modal & temporal logic - examples
W = {w0, w1, w2, w3, w4, w5, w6},
R = {(w0, w1), (w0, w2), (w3, w0),
(w3, w4), (w5, w2), (w6, w2)}
ϑ − set by graph
(w4, []p2) = f; (no following world exists)
(w0, []¬p1) = t;
(w3, []¬p4) = t; (true for w4, w0)
(w0, [] p1) = f; (false for w1, w2)
(w3, p3) = f;
w3
w4
¬p1,¬p3
w0
¬p3
p3
w5
w1
¬p4
p1,¬p4
w2
w6
Semantic Forcing Relation and its negation
Let K be the class of all Kripke models, and M = W, R, ϑ a Kripke model
Let K be the class of all Kripke frames and let F be a Kripke frame
Let Γ be a set of formulae, and ϕ be a formula
Forces We say We write When • ϕ
in a world w forces ϕ w ϕ ϑ(w, ϕ) = t ϑ(w, ϕ) = f
in a model M forces ϕ M ϕ ∀w ∈ W.w ϕ ∃w ∈ W.w ϕ
in a frame F forces ϕ F ϕ ∀ϑ. F, ϑ ϕ ∃ϑ. F, ϑ ϕ
Classicality: either • ϕ or else • ϕ holds for • ∈ {w, M, F}
Exercise: Work out the negation of each fully e.g. M ϕ is ∃w ∈ W.w ¬ϕ
Either w ϕ or else w ¬ϕ holds (Lemma 1)
But this does not apply to all: e.g. either M ϕ or else M ¬ϕ is rarely true.
W ϕ meaning “every frame built out of given W forces ϕ” is not interesting
Introduction to Modal and Temporal Logics 6 December 2007 12
Lecture 5: Tense and Temporal Logics
Tense Logics: interpret []ϕ as “ϕ is true always in the future”.
W represents moments of time
R captures the flow of time
Temporal Logics: similar, but use a more expressive binary modality ϕ Uψ to
capture “ϕ is true at all time points from now until ψ becomes true”.
Shall look at Syntax, Semantics, Hilbert and Tableau Calculi.
Introduction to Modal and Temporal Logics 6 December 2007 80
Tense Logics: Syntax and Semantics
Atomic Formulae: p ::= p0 | p1 | p2 | · · ·
Formulae: ϕ ::= p | ¬ϕ | F ϕ | [F]ϕ | P ϕ | [P]ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ
Boolean connectives interpreted as for modal logic.
Given some Kripke model W, R, ϑ and some w ∈ W, we compute the truth
value of a non-atomic formula by recursion on its shape:
ϑ(w, F ϕ) =
t if ϑ(v, ϕ) = t at some v ∈ W with wRv
f otherwise
ϑ(w, [F]ϕ) =
t if ϑ(v, ϕ) = t at every v ∈ W with wRv
f otherwise
ϑ(w, P ϕ) =
t if ϑ(v, ϕ) = t at some v ∈ W with vRw
f otherwise
ϑ(w, [P]ϕ) =
t if ϑ(v, ϕ) = t at every v ∈ W with vRw
f otherwise
Introduction to Modal and Temporal Logics 6 December 2007 81
Tense Logics: Syntax and Semantics
ϑ(w, F ϕ) =
t if ϑ(v, ϕ) = t at some v ∈ W with wRv
f otherwise
ϑ(w, [F]ϕ) =
t if ϑ(v, ϕ) = t at every v ∈ W with wRv
f otherwise
ϑ(w, P ϕ) =
t if ϑ(v, ϕ) = t at some v ∈ W with vRw
f otherwise
ϑ(w, [P]ϕ) =
t if ϑ(v, ϕ) = t at every v ∈ W with vRw
f otherwise
Example: If W = {w0, w1, w2} and R = {(w0, w1), (w0, w2)} and
ϑ(w1, p3) = t then W, R, ϑ is a Kripke model as pictured below:
w1
w0
R
##GGGGGGGG
R
;;wwwwwwww
w2
ϑ(w0, F p3) = t
ϑ(w2, P F p3) = t
ϑ(w0, [P]p1) = t
Introduction to Modal and Temporal Logics 6 December 2007 82
Modal & temporal logic - examples
W = {w0, w1, w2, w3, w4, w5, w6},
R = {(w0, w1), (w0, w2), (w2, w3),
(w2, w4), (w6, w4), (w5, w4)}
ϑ − set by graph
(w4, [P]p2) = f;
(w2, P F p3) = t;
(w4, P [F]p1) = t; (true for w5, w6)
(w4, P [P]p4) = t; (true for w5, w6; false for w2)
(w0, [F] F p5) = f; (true for w2; false for w1)
¬p4,¬p5
w0
w1
¬p1,p3
w2
¬p3,¬p2
w5
¬p2
w3
¬p1,¬p5
w4
p1,¬p4,p5
w6
¬p5,p2
Different Models of Time
Arbitrary Time: Kt
Reflexive Time: ϕ → F ϕ Transitive Time: F F ϕ → F ϕ
Dense Time: F ϕ → F F ϕ Never Ending Time: [F]ϕ → F ϕ
Backward Linear: F P ϕ → P ϕ ∨ ϕ ∨ F ϕ
Forward Linear: P F ϕ → F ϕ ∨ ϕ ∨ P ϕ
Tableau Calculi also exist but require even more complex loop detection often
called “dynamic blocking”.
Discrete Z, < , Rational Q, < , Real R, < linear and non-reflexive models
of time also possible: see Goldblatt.
Tableau-like calculi exist: see Mosaic Method
Introduction to Modal and Temporal Logics 6 December 2007 84
PLTL: Propositional Linear Temporal Logic
Atomic Formulae: p ::= p0 | p1 | p2 | · · ·
Formulae: ϕ ::= p | ¬ϕ | +ϕ | [F]ϕ | F ϕ | ϕ Uψ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ
Boolean connectives interpreted as for modal logic.
Linear Time Kripke Model: S, σ, R, ϑ
S: non-empty set of states
σ: N → S enumerates S as sequence σ0, σ1, · · · with repetitions when S finite
ϑ: S × Atm → {t, f}
R: is a binary relation over S
Condition: R = σ∗ (R is the reflexive and transitive closure of σ)
Introduction to Modal and Temporal Logics 6 December 2007 85
Semantics of PLTL
ϑ(si, +ϕ) =
t if ϑ(si+1, ϕ) = t
f otherwise
ϑ(si, F ϕ) =
t if ϑ(sj, ϕ) = t for some j ≥ i
f otherwise
ϑ(si, [F]ϕ) =
t if ϑ(sj, ϕ) = t for all j ≥ i
f otherwise
ϑ(si, ϕ Uψ) =
t if ∃k ≥ i.ϑ(sk, ψ) = t & ∀j.i ≤ j < k ⇒ ϑ(sj, ϕ) = t
f otherwise
si si+1 · · · sj · · · sk
p Uq p, ¬q · · · p, ¬q · · · q
Note: when k = i, the state sk is the first state after si where q is true.
Introduction to Modal and Temporal Logics 6 December 2007 86
Semantics of PLTL
ϑ(si, +ϕ) =
t if ϑ(si+1, ϕ) = t
f otherwise
ϑ(si, F ϕ) =
t if ϑ(sj, ϕ) = t for some j ≥ i
f otherwise
ϑ(si, [F]ϕ) =
t if ϑ(sj, ϕ) = t for all j ≥ i
f otherwise
ϑ(si, ϕ Uψ) =
t if ∃k ≥ i.ϑ(sk, ψ) = t & ∀j.i ≤ j < k ⇒ ϑ(sj, ϕ) = t
f otherwise
si si+1 · · · sj · · · sk
¬(p Uq), ¬q ¬q · · · ¬q · · · ¬q q is always false, or
¬(p Uq) ¬q · · · ¬p, ¬q · · · q p false before q true
Note: when k = i, the state sk is the first state after si where q is true. And p is
false in some sj before state sk.
Introduction to Modal and Temporal Logics 6 December 2007 87
Modal & temporal logic - examples
W = {w1...5}; R & ϑ − Set by graph
p,¬q,s
w1
p,¬q
w2
p,¬q
w3
¬p,¬q
w4
q,s
w5
ϑ(w1, ¬qU¬p) = t
ϑ(w1, ¬qUs) = t
ϑ(w1, ¬sUq) = f
ϑ(w2, s) = t
ϑ(w1, ¬pUq) = t
Lecture 6: Fix-point Logics
PLTL: linear time temporal logic
CTL: computation tree logic
PDL: propositional dynamic logic
LCK: logic of common knowledge
Look at CTL but using only one relation R rather than R = σ∗
Introduction to Modal and Temporal Logics 6 December 2007 92