IA008: Computational Logic
7. Modal Logic
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Basic Concepts
Transition Systems
directed graph S = ⟨S,(Ea)a∈A,(Pi)i∈I,s0⟩ with
▸ states S
▸ initial state s0 ∈ S
▸ edge relations Ea with edge colours a ∈ A (‘actions’)
▸ unary predicates Pi with vertex colours i ∈ I (‘properties’)
a
b
b
b
a
aa,b
pq
Modal logic
Propositional logic with modal operators
▸ ⟨a⟩φ ‘there exists an a-successor where φ holds’
▸ [a]φ ‘φ holds in every a-successor’
Notation: φ, ◻φ if there are no edge labels
Formal semantics
S,s ⊧ P :iff s ∈ P
S,s ⊧ φ ∧ ψ :iff S,s ⊧ φ and S,s ⊧ ψ
S,s ⊧ φ ∨ ψ :iff S,s ⊧ φ or S,s ⊧ ψ
S,s ⊧ ¬φ :iff S,s ⊭ φ
S,s ⊧ ⟨a⟩φ :iff there is s →a
t such that S,t ⊧ φ
S,s ⊧ [a]φ :iff for all s →a
t , we have S,t ⊧ φ
Examples
P ∧ Q ‘吀he state is in P and there exists a transition to Q.’
[a] ‘吀he state has no outgoing a-transition.’
Interpretations
▸ Temporal Logic talks about time:
▸ states: points in time (discrete/continuous)
▸ φ ‘sometime in the future φ holds’
▸ ◻φ ‘always in the future φ holds’
▸ Epistemic Logic talks about knowledge:
▸ states: possible worlds
▸ φ ‘φ might be true’
▸ ◻φ ‘φ is certainly true’
Examples: Temporal Logic
system S = ⟨S,<, ¯P⟩
▸ “P never holds.”
Examples: Temporal Logic
system S = ⟨S,<, ¯P⟩
▸ “P never holds.”
¬P ∧ ¬ P
▸ “A昀ter every P there is some Q.”
Examples: Temporal Logic
system S = ⟨S,<, ¯P⟩
▸ “P never holds.”
¬P ∧ ¬ P
▸ “A昀ter every P there is some Q.”
(P → Q) ∧ ◻(P → Q)
▸ “Once P holds, it holds forever.”
Examples: Temporal Logic
system S = ⟨S,<, ¯P⟩
▸ “P never holds.”
¬P ∧ ¬ P
▸ “A昀ter every P there is some Q.”
(P → Q) ∧ ◻(P → Q)
▸ “Once P holds, it holds forever.”
(P → ◻P) ∧ ◻(P → ◻P)
▸ “吀here are infinitely many P.” (for the order ⟨N,<⟩)
Examples: Temporal Logic
system S = ⟨S,<, ¯P⟩
▸ “P never holds.”
¬P ∧ ¬ P
▸ “A昀ter every P there is some Q.”
(P → Q) ∧ ◻(P → Q)
▸ “Once P holds, it holds forever.”
(P → ◻P) ∧ ◻(P → ◻P)
▸ “吀here are infinitely many P.” (for the order ⟨N,<⟩)
◻ P
Translation to first-order logic
Proposition
For every formula φ of propositional modal logic, there exists a
formula φ∗
(x) of first-order logic such that
S,s ⊧ φ iff S ⊧ φ∗
(s) .
Proof
Translation to first-order logic
Proposition
For every formula φ of propositional modal logic, there exists a
formula φ∗
(x) of first-order logic such that
S,s ⊧ φ iff S ⊧ φ∗
(s) .
Proof
P∗
= P(x)
(φ ∧ ψ)∗
= φ∗
(x) ∧ ψ∗
(x)
(φ ∨ ψ)∗
= φ∗
(x) ∨ ψ∗
(x)
(¬φ)∗
= ¬φ∗
(x)
(⟨a⟩φ)∗
= ∃y[Ea(x,y) ∧ φ∗
(y)]
([a]φ)∗
= ∀y[Ea(x,y) → φ∗
(y)]
Bisimulation
S and T transition systems
Z ⊆ S × T is a bisimulation if, for all ⟨s,t⟩ ∈ Z,
(local) s ∈ P ⇔ t ∈ P
(forth) for every s →a
s′
, exists t →a
t′
with ⟨s′
,t′
⟩ ∈ Z,
(back) for every t →a
t′
, exists s →a
s′
with ⟨s′
,t′
⟩ ∈ Z.
S,s and T,t are bisimilar if there is a bisimulation Z with ⟨s,t⟩ ∈ Z.
s
s′
t
t′
a a
Z
Z
Examples
Examples
Examples
Examples
Unravelling
b
a
a
S
b a
a b
b a a b
U(S)
Lemma
S and U(S) are bisimilar.
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
(boolean combinations) by inductive hypothesis
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
(boolean combinations) by inductive hypothesis
(φ = ⟨a⟩ψ) S,s ⊧ ⟨a⟩ψ
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
(boolean combinations) by inductive hypothesis
(φ = ⟨a⟩ψ) S,s ⊧ ⟨a⟩ψ
⇒ ex. s →a
s′
with S,s′
⊧ ψ
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
(boolean combinations) by inductive hypothesis
(φ = ⟨a⟩ψ) S,s ⊧ ⟨a⟩ψ
⇒ ex. s →a
s′
with S,s′
⊧ ψ
S,s ∼ T,t ⇒ ex. t →a
t′
with S,s′
∼ T,t′
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
(boolean combinations) by inductive hypothesis
(φ = ⟨a⟩ψ) S,s ⊧ ⟨a⟩ψ
⇒ ex. s →a
s′
with S,s′
⊧ ψ
S,s ∼ T,t ⇒ ex. t →a
t′
with S,s′
∼ T,t′
⇒ T,t′
⊧ ψ
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
Proof (for ⇒) induction on φ
(φ = P) s ∈ P ⇔ t ∈ P
(boolean combinations) by inductive hypothesis
(φ = ⟨a⟩ψ) S,s ⊧ ⟨a⟩ψ
⇒ ex. s →a
s′
with S,s′
⊧ ψ
S,s ∼ T,t ⇒ ex. t →a
t′
with S,s′
∼ T,t′
⇒ T,t′
⊧ ψ
⇒ T,t ⊧ ⟨a⟩ψ
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
吀heorem
Every satisfiable modal formula has a model that is a finite tree.
Bisimulation invariance
吀heorem
Two finite transition systems S,s and T,t are bisimilar if, and only
if,
S,s ⊧ φ ⇔ T,t ⊧ φ, for every modal formula φ.
吀heorem
Every satisfiable modal formula has a model that is a finite tree.
Definition
A formula φ(x) is bisimulation invariant if
S,s ∼ T,t implies S ⊧ φ(s) ⇔ T ⊧ φ(t) .
吀heorem
A first-order formula φ is equivalent to a modal formula if, and only
if, it is bisimulation invariant.
First-Order Modal Logic
Syntax
first-order logic with modal operators ⟨a⟩φ and [a]φ
First-Order Modal Logic
Syntax
first-order logic with modal operators ⟨a⟩φ and [a]φ
Models
transistion systems where each state s is labelled with a
Σ-structure As such that
s →a
t implies As ⊆ At
First-Order Modal Logic
Syntax
first-order logic with modal operators ⟨a⟩φ and [a]φ
Models
transistion systems where each state s is labelled with a
Σ-structure As such that
s →a
t implies As ⊆ At
Examples
▸ ◻∀xφ(x) → ∀x ◻ φ(x) is valid.
▸ ∀x ◻ φ(x) → ◻∀xφ(x) is not valid.
Tableaux
吀he Entailment Relation
Consequence
ψ is a consequence of Γ (Γ ⊧ φ) if, and only if, for all transition
systems S,
S,s ⊧ φ, for all s ∈ S and φ ∈ Γ ,
implies that
S,s ⊧ ψ, for all s ∈ S .
Tableau Proofs
Statements
s ⊧ φ s ⊭ φ s →a
t
s,t state labels, φ a modal formula
Rules
s ⊧ φ
s ⊧ ψ0
...
s ⊭ θ0
s ⊭ ψm s ⊧ θn
Tableaux
Construction
A tableau for a formula φ is constructed as follows:
▸ start with s0 ⊭ φ
▸ choose a branch of the tree
▸ choose a statement s ⊧ ψ/s ⊭ ψ on the branch
▸ choose a rule with head s ⊧ ψ/s ⊭ ψ
▸ add it at the bottom of the branch
▸ repeat until every branch contains both statements s ⊧ ψ and
s ⊭ ψ for some formula ψ
Tableaux
Construction
A tableau for a formula φ is constructed as follows:
▸ start with s0 ⊭ φ
▸ choose a branch of the tree
▸ choose a statement s ⊧ ψ/s ⊭ ψ on the branch
▸ choose a rule with head s ⊧ ψ/s ⊭ ψ
▸ add it at the bottom of the branch
▸ repeat until every branch contains both statements s ⊧ ψ and
s ⊭ ψ for some formula ψ
Tableaux with premises Γ
▸ choose a branch, a state s on the branch, a premise ψ ∈ Γ, and
add s ⊧ ψ to the branch
Rules
s ⊧ ¬φ
s ⊭ φ
s ⊭ ¬φ
s ⊧ φ
s ⊧ φ ∧ ψ
s ⊧ φ
s ⊧ ψ
s ⊭ φ ∧ ψ
s ⊭ φ s ⊭ ψ
s ⊧ φ ∨ ψ
s ⊧ φ s ⊧ ψ
s ⊭ φ ∨ ψ
s ⊭ φ
s ⊭ ψ
s ⊧ φ → ψ
s ⊭ φ s ⊧ ψ
s ⊭ φ → ψ
s ⊧ φ
s ⊭ ψ
s ⊧ φ ↔ ψ
s ⊧ φ
s ⊧ ψ
s ⊭ φ
s ⊭ ψ
s ⊭ φ ↔ ψ
s ⊧ φ
s ⊭ ψ
s ⊭ φ
s ⊧ ψ
Rules
s ⊧ ⟨a⟩φ
s →a
t
t ⊧ φ
s ⊭ ⟨a⟩φ
t′
⊭ φ
s ⊧ [a]φ
t′
⊧ φ
s ⊭ [a]φ
s →a
t
t ⊭ φ
s ⊧ ∀xφ
s ⊧ φ[x ↦ u]
s ⊭ ∀xφ
s ⊭ φ[x ↦ c]
s ⊧ ∃xφ
s ⊧ φ[x ↦ c]
s ⊭ ∃xφ
s ⊭ φ[x ↦ u]
t a new state, t′
every state with entry s →a
t′
on the branch,
c a new constant symbol, u an arbitrary term
Example ⊧ ◻(φ → ψ) → (◻φ → ◻ψ)
Example ⊧ ◻(φ → ψ) → (◻φ → ◻ψ)
s ⊭ ◻(φ → ψ) → (◻φ → ◻ψ)
s ⊧ ◻(φ → ψ)
s ⊭ ◻φ → ◻ψ
s ⊧ ◻φ
s ⊭ ◻ψ
s → t
t ⊭ ψ
t ⊧ φ
t ⊧ φ → ψ
t ⊭ φ t ⊧ ψ
Example φ ⊧ ◻φ
Example φ ⊧ ◻φ
s ⊭ ◻φ
s → t
t ⊭ φ
t ⊧ φ
Example ⊧ ◻∀xφ → ∀x ◻ φ
Example ⊧ ◻∀xφ → ∀x ◻ φ
s ⊭ ◻∀xφ → ∀x ◻ φ
s ⊧ ◻∀xφ
s ⊭ ∀x ◻ φ
s ⊭ ◻φ[x ↦ c]
s → t
t ⊭ φ[x ↦ c]
t ⊧ ∀xφ
t ⊧ φ[x ↦ c]
Soundness and Completeness
吀heorem
A modal formula φ is a consequence of Γ if, and only if, there exists a
tableau T for φ with premises Γ where every branch is contradictory.
Soundness and Completeness
吀heorem
A modal formula φ is a consequence of Γ if, and only if, there exists a
tableau T for φ with premises Γ where every branch is contradictory.
吀heorem
Satisfiability for propositional modal logic is in deterministic linear
space.
吀heorem
Satisfiability for first-order modal logic is undecidable.
Temporal Logics
Linear Temporal Logic (LTL)
Speaks about paths. P → → → P,Q → Q → → ⋯
Syntax
▸ atomic predicates P,Q,...
▸ boolean operations ∧,∨,¬
▸ next Xφ
▸ until φUψ
▸ finally Fφ = ⊺Uφ
▸ generally Gφ = ¬F¬φ
Examples
FP a state in P is reachable
GFP we can reach infinitely many states in P
(¬P)U(P ∧ Q) the first reachable state in P is also in Q
Linear Temporal Logic (LTL)
吀heorem
Let L be a set of paths. 吀he following statements are equivalent:
▸ L can be defined in LTL.
▸ L can be defined in first-order logic.
▸ L can be defined by a star-free regular expression.
Linear Temporal Logic (LTL)
吀heorem
Let L be a set of paths. 吀he following statements are equivalent:
▸ L can be defined in LTL.
▸ L can be defined in first-order logic.
▸ L can be defined by a star-free regular expression.
Translation LTL to FO
P∗
= P(x)
(φ ∧ ψ)∗
= φ∗
(x) ∧ ψ∗
(x)
(φ ∨ ψ)∗
= φ∗
(x) ∨ ψ∗
(x)
(¬φ)∗
= ¬φ∗
(x)
(Xφ)∗
= ∃y[x < y ∧ ¬∃z(x < z ∧ z < y) ∧ φ∗
(y)]
(φUψ)∗
= ∃y[x ≤ y ∧ ψ∗
(y) ∧ ∀z[x ≤ z ∧ z < y → φ∗
(z)]]
Linear Temporal Logic (LTL)
吀heorem
Satisfiablity of LTL formulae is PSPACE-complete.
吀heorem
Model checking S,s ⊧ φ for LTL is PSPACE-complete. It can be
done in
time O( S ⋅ 2O( φ )
) or space O(( φ + log S )2
) .
Linear Temporal Logic (LTL)
吀heorem
Satisfiablity of LTL formulae is PSPACE-complete.
吀heorem
Model checking S,s ⊧ φ for LTL is PSPACE-complete. It can be
done in
time O( S ⋅ 2O( φ )
) or space O(( φ + log S )2
) .
Formula complexity: PSPACE-complete
Data complexity: NLOGSPACE-complete
Computation Tree Logic (CTL and CTL*)
Applies LTL-formulae to the branches of a tree.
Syntax (of CTL*)
▸ state formulae φ:
φ = P φ ∧ φ φ ∨ φ ¬φ Aψ Eψ
▸ path formulae ψ:
ψ = φ ψ ∧ ψ ψ ∨ ψ ¬ψ Xψ ψUψ Fψ Gψ
Examples
EFP a state in P is reachable
AFP every branch contains a state in P
EGFP there is a branch with infinitely many P
EGEFP there is a branch such that we can reach P from every
of its states
Computation Tree Logic (CTL and CTL*)
吀heorem
Satisfiability for CTL is EXPTIME-complete.
Model checking S,s ⊧ φ for CTL is P-complete. It can be done in
time O( φ ⋅ S ) or space O( φ ⋅ log2
( φ ⋅ S )) .
Data complexity: NLOGSPACE-complete
Computation Tree Logic (CTL and CTL*)
吀heorem
Satisfiability for CTL is EXPTIME-complete.
Model checking S,s ⊧ φ for CTL is P-complete. It can be done in
time O( φ ⋅ S ) or space O( φ ⋅ log2
( φ ⋅ S )) .
Data complexity: NLOGSPACE-complete
吀heorem
Satisfiability for CTL* is 2EXPTIME-complete.
Model checking S,s ⊧ φ for CTL* is PSPACE-complete. It can be
done in
time O( S 2
⋅ 2O( φ )
) or space O( φ ( φ + log S )2
) .
Formula complexity: PSPACE-complete
Data complexity: NLOGSPACE-complete
Fixed points
吀heorem (Knaster, Tarski)
Let ⟨A,≤⟩ be a complete partial order and f A → A monotone.
吀hen f has a least and a greatest fixed point and
lfp(f) = lim
α→∞
fα
( ) and gfp(f) = lim
α→∞
fα
(⊺)
Fixed points
吀heorem (Knaster, Tarski)
Let ⟨A,≤⟩ be a complete partial order and f A → A monotone.
吀hen f has a least and a greatest fixed point and
lfp(f) = lim
α→∞
fα
( ) and gfp(f) = lim
α→∞
fα
(⊺)
Examples ⟨℘(N),⊆⟩
• f(X) = (X ∖ A) ∪ B
Fixed points
吀heorem (Knaster, Tarski)
Let ⟨A,≤⟩ be a complete partial order and f A → A monotone.
吀hen f has a least and a greatest fixed point and
lfp(f) = lim
α→∞
fα
( ) and gfp(f) = lim
α→∞
fα
(⊺)
Examples ⟨℘(N),⊆⟩
• f(X) = (X ∖ A) ∪ B
lfp(f) = B and gfp(f) = (N ∖ A) ∪ B
• f(X) = { y y ≤ x ∈ X }
Fixed points
吀heorem (Knaster, Tarski)
Let ⟨A,≤⟩ be a complete partial order and f A → A monotone.
吀hen f has a least and a greatest fixed point and
lfp(f) = lim
α→∞
fα
( ) and gfp(f) = lim
α→∞
fα
(⊺)
Examples ⟨℘(N),⊆⟩
• f(X) = (X ∖ A) ∪ B
lfp(f) = B and gfp(f) = (N ∖ A) ∪ B
• f(X) = { y y ≤ x ∈ X }
fixed points: ∅, {0}, {0,1},..., {0,...,n},..., N
• f(X) = N ∖ X
Fixed points
吀heorem (Knaster, Tarski)
Let ⟨A,≤⟩ be a complete partial order and f A → A monotone.
吀hen f has a least and a greatest fixed point and
lfp(f) = lim
α→∞
fα
( ) and gfp(f) = lim
α→∞
fα
(⊺)
Examples ⟨℘(N),⊆⟩
• f(X) = (X ∖ A) ∪ B
lfp(f) = B and gfp(f) = (N ∖ A) ∪ B
• f(X) = { y y ≤ x ∈ X }
fixed points: ∅, {0}, {0,1},..., {0,...,n},..., N
• f(X) = N ∖ X has no fixed points
Ordinals
0,1,2,3,...
Ordinals
0,1,2,3,... ω
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,... ω1,... ω2,...
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,... ω1,... ω2,...
3 Kinds
• 0
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,... ω1,... ω2,...
3 Kinds
• 0
• successor α + 1
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,... ω1,... ω2,...
3 Kinds
• 0
• successor α + 1
• limit δ
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,... ω1,... ω2,...
3 Kinds
• 0
• successor α + 1
• limit δ
Proposition
Every non-empty set of ordinals has a least element.
Ordinals
0,1,2,3,... ω, ω + 1, ω + 2,... ω + ω = ω2, ω2 + 1, ω2 + 2,...
ω3,... ω4,... ω5,... ωω = ω2
,... ω3
,... ω4
,...
ωω
,... ωωω
,... ωωωω
,... ε,... ω1,... ω2,...
3 Kinds
• 0
• successor α + 1
• limit δ
Iteration
f0
(x) = x,
fα+1
(x) = f(fα
(x)) ,
fδ
(x) = sup
α<δ
fα
(x) , for limit ordinals δ .
(for gfp, take inf instead of sup)
Proof
Monotonicity fα
( ) ≤ fβ
( ) for α ≤ β
induction on α
(α = 0) ≤ fβ
( ) ( is the least element)
Proof
Monotonicity fα
( ) ≤ fβ
( ) for α ≤ β
induction on α
(α = 0) ≤ fβ
( ) ( is the least element)
(α = α′
+ 1) If β = β′
+ 1, we have
fα′
( ) ≤ fβ′
( ) ⇒ fα′+1
( ) ≤ fβ′+1
( ) . (f is monotone)
Proof
Monotonicity fα
( ) ≤ fβ
( ) for α ≤ β
induction on α
(α = 0) ≤ fβ
( ) ( is the least element)
(α = α′
+ 1) If β = β′
+ 1, we have
fα′
( ) ≤ fβ′
( ) ⇒ fα′+1
( ) ≤ fβ′+1
( ) . (f is monotone)
If β is a limit, we have
fα
( ) ≤ sup
γ<β
fγ
( ) = fβ
( ) . (definition of supremum)
Proof
Monotonicity fα
( ) ≤ fβ
( ) for α ≤ β
induction on α
(α = 0) ≤ fβ
( ) ( is the least element)
(α = α′
+ 1) If β = β′
+ 1, we have
fα′
( ) ≤ fβ′
( ) ⇒ fα′+1
( ) ≤ fβ′+1
( ) . (f is monotone)
If β is a limit, we have
fα
( ) ≤ sup
γ<β
fγ
( ) = fβ
( ) . (definition of supremum)
(α limit) For γ < α, we have fγ
( ) ≤ fβ
( ). Hence,
fα
( ) = sup
γ<α
fγ
( ) ≤ fβ
( ) . (inductive hypothesis)
Proof
Existence
exists α with fα
( ) = fα+1
( ) (there are only A different values)
Proof
Existence
exists α with fα
( ) = fα+1
( ) (there are only A different values)
Least fixed point
a = f(a) fixed point, fα
( ) = fα+1
( )
Proof
Existence
exists α with fα
( ) = fα+1
( ) (there are only A different values)
Least fixed point
a = f(a) fixed point, fα
( ) = fα+1
( )
≤ a
Proof
Existence
exists α with fα
( ) = fα+1
( ) (there are only A different values)
Least fixed point
a = f(a) fixed point, fα
( ) = fα+1
( )
≤ a ⇒ fα
( ) ≤ fα
(a) = a (fα
monotone, by induction on α)
吀he modal μ-calculus (Lμ)
Adds recursion to modal logic.
Syntax
φ = P φ ∧ φ φ ∨ φ ¬φ ⟨a⟩φ [a]φ μX.φ(X) νX.φ(X)
(X positive in μX.φ(X) and νX.φ(X))
吀he modal μ-calculus (Lμ)
Adds recursion to modal logic.
Syntax
φ = P φ ∧ φ φ ∨ φ ¬φ ⟨a⟩φ [a]φ μX.φ(X) νX.φ(X)
(X positive in μX.φ(X) and νX.φ(X))
Semantics
Fφ(X) = { s ∈ S S,s ⊧ φ(X)}
μX.φ(X) X0 = ∅ , Xi+1 = Fφ(Xi)
νX.φ(X) X0 = S , Xi+1 = Fφ(Xi)
吀he modal μ-calculus (Lμ)
Adds recursion to modal logic.
Syntax
φ = P φ ∧ φ φ ∨ φ ¬φ ⟨a⟩φ [a]φ μX.φ(X) νX.φ(X)
(X positive in μX.φ(X) and νX.φ(X))
Semantics
Fφ(X) = { s ∈ S S,s ⊧ φ(X)}
μX.φ(X) X0 = ∅ , Xi+1 = Fφ(Xi)
νX.φ(X) X0 = S , Xi+1 = Fφ(Xi)
Examples
μX(P ∨ X) a state in P is reachable
νX(P ∧ X) there is a branch with all states in P
Examples
μX(P ∨ X) a state in P is reachable
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o P
Examples
μX(P ∨ X) a state in P is reachable
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o P
Examples
μX(P ∨ X) a state in P is reachable
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o P
Examples
μX(P ∨ X) a state in P is reachable
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o P
Examples
μX(P ∨ X) a state in P is reachable
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o P
Examples
μX(P ∨ X) a state in P is reachable
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Examples
νX(P ∧ X) there is a branch with all states in P
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
P
P
P
P
P
P
P
P
P
P
P
P
Expressive power
吀heorem
For every CTL*-formula φ there exists an equivalent formula φ∗
of
the modal μ-calculus.
Expressive power
吀heorem
For every CTL*-formula φ there exists an equivalent formula φ∗
of
the modal μ-calculus.
Proof (for CTL)
P∗
= P
(φ ∧ ψ)∗
= φ∗
∧ ψ∗
(φ ∨ ψ)∗
= φ∗
∨ ψ∗
(¬φ)∗
= ¬φ∗
(EXφ)∗
= φ∗
(AXφ)∗
= ◻φ∗
(EφUψ)∗
= μX[ψ∗
∨ (φ∗
∧ X)]
(AφUψ)∗
= μX[ψ∗
∨ (φ∗
∧ ◻X)]
吀he modal μ-calculus (Lμ)
吀heorem
A regular tree language can be defined in the modal μ-calculus if,
and only if, it is bisimulation invariant.
吀heorem
Satisfiability of μ-calculus formulae is decidable and complete for
exponential time.
Model checking S,s ⊧ φ for the modal μ-calculus can be done in
time O(( φ ⋅ S ) φ
).
(吀he satisfiability algorithm uses tree automata and parity games.)
Parity Games
G = ⟨V ,V◻,E,Ω⟩ Ω V → N
Infinite plays v0,v1,... are won by Player if
liminf
n→∞
Ω(vn) is even.
3
2
5
2
1
2
0
3
2
3
Parity Games
G = ⟨V ,V◻,E,Ω⟩ Ω V → N
Infinite plays v0,v1,... are won by Player if
liminf
n→∞
Ω(vn) is even.
3
2
5
2
1
2
0
3
2
3
Parity Games
G = ⟨V ,V◻,E,Ω⟩ Ω V → N
Infinite plays v0,v1,... are won by Player if
liminf
n→∞
Ω(vn) is even.
吀heorem
Parity games are positionally determined: from each position some
player has a positional/memory-less winning strategy.
Parity Games
G = ⟨V ,V◻,E,Ω⟩ Ω V → N
Infinite plays v0,v1,... are won by Player if
liminf
n→∞
Ω(vn) is even.
吀heorem
Parity games are positionally determined: from each position some
player has a positional/memory-less winning strategy.
吀heorem
Computing the winning region of a parity game with n positions and
d priorities can be done in time nO(log d)
.
Model-Checking Games
game for S,s0 ⊧ φ? (φ μ-formula in negation normal form)
Model-Checking Games
game for S,s0 ⊧ φ? (φ μ-formula in negation normal form)
Positions
Player : ⟨s,ψ⟩ for s ∈ S and ψ a subformula
ψ = ψ0 ∨ ψ1 , ψ = P and s ∉ P , ψ = μX.ψ0 ,
ψ = ⟨a⟩ψ0 , ψ = ¬P and s ∈ P , ψ = νX.ψ0 ,
ψ = X .
Player ◻: [s,ψ] for s ∈ S and ψ a subformula
ψ = ψ0 ∧ ψ1 , ψ = P and s ∈ P ,
ψ = [a]ψ0 , ψ = ¬P and s ∉ P .
Model-Checking Games
game for S,s0 ⊧ φ? (φ μ-formula in negation normal form)
Positions
Player : ⟨s,ψ⟩ for s ∈ S and ψ a subformula
ψ = ψ0 ∨ ψ1 , ψ = P and s ∉ P , ψ = μX.ψ0 ,
ψ = ⟨a⟩ψ0 , ψ = ¬P and s ∈ P , ψ = νX.ψ0 ,
ψ = X .
Player ◻: [s,ψ] for s ∈ S and ψ a subformula
ψ = ψ0 ∧ ψ1 , ψ = P and s ∈ P ,
ψ = [a]ψ0 , ψ = ¬P and s ∉ P .
Initial position ⟨s0,φ⟩ or [s0,φ]
Model-Checking Games
game for S,s0 ⊧ φ? (φ μ-formula in negation normal form)
Edges ((s,ψ) means either ⟨s,ψ⟩ or [s,ψ].)
⟨s,ψ0 ∨ ψ1⟩ → (s,ψi) ,
[s,ψ0 ∧ ψ1] → (s,ψi) ,
⟨s,μX.ψ⟩ → ψ,
⟨s,νX.ψ⟩ → ψ,
⟨s,X⟩ → ⟨s,μX.ψ⟩ or ⟨s,νX.ψ⟩ ,
⟨s,⟨a⟩ψ⟩ → (t,ψ) for every s →a
t ,
[s,[a]ψ] → (t,ψ) for every s →a
t .
Model-Checking Games
game for S,s0 ⊧ φ? (φ μ-formula in negation normal form)
Edges ((s,ψ) means either ⟨s,ψ⟩ or [s,ψ].)
⟨s,ψ0 ∨ ψ1⟩ → (s,ψi) ,
[s,ψ0 ∧ ψ1] → (s,ψi) ,
⟨s,μX.ψ⟩ → ψ,
⟨s,νX.ψ⟩ → ψ,
⟨s,X⟩ → ⟨s,μX.ψ⟩ or ⟨s,νX.ψ⟩ ,
⟨s,⟨a⟩ψ⟩ → (t,ψ) for every s →a
t ,
[s,[a]ψ] → (t,ψ) for every s →a
t .
Priorities (all other priorities big)
Ω(⟨s,μX.ψ⟩) = 2k + 1 , if inside of k fixed points.
Ω(⟨s,νX.ψ⟩) = 2k .
Model-Checking Games
S = s t P φ = μX(P ∨ X)
Model-Checking Games
S = s t P φ = μX(P ∨ X)
⟨s, μX(P ∨ X)⟩
⟨t, μX(P ∨ X)⟩
⟨s, P ∨ X⟩
⟨t, P ∨ X⟩
⟨s, P⟩
[t, P]
⟨s, X⟩
⟨t, X⟩
⟨s, X⟩
⟨t, X⟩
1
1
Model-Checking Games
S = s t P φ = νX( X ∧ μY(P ∨ Y))
Model-Checking Games
S = s t P φ = νX( X ∧ μY(P ∨ Y))
⟨s, φ⟩ [s, X ∧ μY(. . .)] ⟨s, μY(P ∨ Y)⟩
⟨s, X⟩
⟨s, P ∨ Y⟩
⟨s, P⟩
⟨s, Y⟩
⟨s, Y⟩
⟨s, X⟩
⟨t, φ⟩ [t, X ∧ μY(. . .)] ⟨t, μY(P ∨ Y)⟩
⟨t, X⟩
⟨t, P ∨ Y⟩
[t, P]
⟨t, Y⟩
⟨t, Y⟩
⟨t, X⟩
0
3
0
3
Description Logics
Description Logic
General Idea
Extend modal logic with operations that are not
bisimulation-invariant.
Applications
Knowledge representation, deductive databases, system modelling,
semantic web
Ingredients
▸ individuals: elements (Anna, John, Paul, Marry,…)
▸ concepts: unary predicates (person, male, female,…)
▸ roles: binary relations (has_child, is_married_to,…)
▸ TBox: terminology definitions
▸ ABox: assertions about the world
Example
TBox
man = person ∧ male
woman = person ∧ female
father = man ∧ ∃has_child.person
mother = woman ∧ ∃has_child.person
ABox
man(John)
man(Paul)
woman(Anna)
woman(Marry)
has_child(Anna,Paul)
is_married_to(Anna,John)
Syntax
Concepts
φ = P ⊺ ¬φ φ ∧ φ φ ∨ φ ∀Rφ ∃Rφ (≥nR) (≤nR)
Terminology axioms
φ ⊑ ψ φ ≡ ψ
TBox Axioms of the form P ≡ φ.
Assertions
φ(a) R(a,b)
Extensions
▸ operations on roles: R ∩ S, R ∪ S, R ○ S, ¬R, R+
, R∗
, R−
▸ extended number restrictions: (≥nR)φ, (≤nR)φ
Algorithmic Problems
▸ Satisfiability: Is φ satisfiable?
▸ Subsumption: φ ⊧ ψ?
▸ Equivalence: φ ≡ ψ?
▸ Disjointness: φ ∧ ψ unsatisfiable?
All problems can be solved with standard methods like tableaux or
tree automata.
Semantic Web: OWL (functional syntax)
Ontology(
Class(pp:man complete
intersectionOf(pp:person pp:male))
Class(pp:woman complete
intersectionOf(pp:person pp:female))
Class(pp:father complete
intersectionOf(pp:man
restriction(pp:has_child pp:person)))
Class(pp:mother complete
intersectionOf(pp:woman
restriction(pp:has_child pp:person)))
Individual(pp:John type(pp:man))
Individual(pp:Paul type(pp:man))
Individual(pp:Anna type(pp:woman)
value(pp:has_child pp:Paul)
value(pp:is_married_to pp:John))
Individual(pp:Marry type(pp:woman))
)