IA008: Computational Logic
6. 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 ‘The state is in P and there exists a transition to Q.’
[a] ‘The 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
▸ “After every P there is some Q.”
Examples: Temporal Logic
system S = ⟨S, ≤, ¯P⟩
▸ “P never holds.”
¬ P
▸ “After every P there is some Q.”
◻(P → Q)
▸ “Once P holds, it holds forever.”
Examples: Temporal Logic
system S = ⟨S, ≤, ¯P⟩
▸ “P never holds.”
¬ P
▸ “After every P there is some Q.”
◻(P → Q)
▸ “Once P holds, it holds forever.”
◻(P → ◻P)
▸ “There are infinitely many P.”
Examples: Temporal Logic
system S = ⟨S, ≤, ¯P⟩
▸ “P never holds.”
¬ P
▸ “After every P there is some Q.”
◻(P → Q)
▸ “Once P holds, it holds forever.”
◻(P → ◻P)
▸ “There are infinitely many P.”
◻ 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
Theorem
Two finite transition systems S, s and T, t are bisimilar if, and only if,
S, s ⊧ φ ⇔ T, t ⊧ φ , for every modal formula φ .
Definition
A formula φ(x) is bisimulation invariant if
S, s ∼ T, t implies S ⊧ φ(s) ⇔ T ⊧ φ(t) .
Theorem
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
Tableau Proofs
Statements
s ⊧ φ s ⊭ φ s →a
t
s, t state labels, φ a modal formula
Rules
s ⊧ φ
s ⊧ ψ
. . .
s ⊭ ϑ
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 φ ⊧ ◻φ
s ⊭ φ
s → t
t ⊭ φ
t ⊧ φ
Example ⊧ ◻(φ → ψ) → (◻φ → ◻ψ)
s ⊭ (φ → ψ) → ( φ → ψ)
s ⊧ (φ → ψ)
s ⊭ φ → ψ
s ⊧ φ
s ⊭ ψ
s → t
t ⊭ ψ
t ⊧ φ
t ⊧ φ → ψ
t ⊭ φ t ⊧ ψ
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
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 .
Soundness and Completeness
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 .
Theorem
A modal formula φ is a consequence of Γ if, and only if, there exists a
tableau T for φ with premises Γ where every branch is contradictory.
Complexity
Theorem
Satisfiability for propositional modal logic is in deterministic linear
space.
Theorem
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)
Theorem
Let L be a set of paths. The 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)
Theorem
Let L be a set of paths. The 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)
Theorem
Satisfiablity of LTL formulae is PSPACE-complete.
Theorem
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)
Theorem
Satisfiablity of LTL formulae is PSPACE-complete.
Theorem
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*)
Theorem
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*)
Theorem
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
Theorem
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
Theorem (Knaster, Tarski)
Let ⟨A, ≤⟩ be a complete partial order and f A → A monotone. Then
f has a least and a greatest fixed point and
lfp(f ) = lim
α→∞
f α
( ) and gfp(f ) = lim
α→∞
f α
(⊺)
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 δ
Proposition
Every non-empty set of ordinals has a least element.
Iteration
f 0
(x) = x ,
f α+1
(x) = f (f α
(x)) ,
f δ
(x) = sup
α<δ
f α
(x) , for limit ordinals δ .
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
⇒ f δ
( ) = supα<δ f α
( ) ≤ f δ+1
( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
⇒ f δ
( ) = supα<δ f α
( ) ≤ f δ+1
( )
f α
( ) ≤ supβ<δ f β
( ) = f δ
( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
⇒ f δ
( ) = supα<δ f α
( ) ≤ f δ+1
( )
f α
( ) ≤ supβ<δ f β
( ) = f δ
( )
Existence exists α with f α
( ) = f α+1
( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
⇒ f δ
( ) = supα<δ f α
( ) ≤ f δ+1
( )
f α
( ) ≤ supβ<δ f β
( ) = f δ
( )
Existence exists α with f α
( ) = f α+1
( )
Least fixed point
a = f (a) fixed point, f α
( ) = f α+1
( )
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
⇒ f δ
( ) = supα<δ f α
( ) ≤ f δ+1
( )
f α
( ) ≤ supβ<δ f β
( ) = f δ
( )
Existence exists α with f α
( ) = f α+1
( )
Least fixed point
a = f (a) fixed point, f α
( ) = f α+1
( )
≤ a
Proof
Monotonicity f α
( ) ≤ f β
( ) for α ≤ β
≤ f ( )
f α
( ) ≤ f β
( ) ⇒ f α+1
( ) ≤ f β+1
( )
f α
( ) ≤ f δ
( ) for all α < δ
⇒ f α+1
( ) ≤ f δ+1
( )
⇒ f δ
( ) = supα<δ f α
( ) ≤ f δ+1
( )
f α
( ) ≤ supβ<δ f β
( ) = f δ
( )
Existence exists α with f α
( ) = f α+1
( )
Least fixed point
a = f (a) fixed point, f α
( ) = f α+1
( )
≤ a ⇒ f α
( ) ≤ f α
(a) = a
The modal µ-calculus (Lµ)
Adds recursion to modal logic.
Syntax
φ = P φ ∧ φ φ ∨ φ ¬φ ⟨a⟩φ [a]φ µX.φ(X) νX.φ(X)
(X positive in µX.φ(X) and νX.φ(X))
The 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)
The 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
Theorem
For every CTL*-formula φ there exists an equivalent formula φ∗
of the
modal µ-calculus.
Expressive power
Theorem
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)]
The modal µ-calculus (Lµ)
Theorem
A regular tree language can be defined in the modal µ-calculus if, and
only if, it is bisimulation invariant.
Theorem
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 ) φ
).
(The 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.










Parity Games
G = ⟨V , V◻, E, Ω⟩ Ω V → N
Infinite plays v0, v1, . . . are won by Player if
liminf
n→∞
Ω(vn) is even.










Parity Games
G = ⟨V , V◻, E, Ω⟩ Ω V → N
Infinite plays v0, v1, . . . are won by Player if
liminf
n→∞
Ω(vn) is even.
Theorem
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.
Theorem
Parity games are positionally determined: from each position some
player has a positional/memory-less winning strategy.
Theorem
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⟩


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, φ⟩ [s, ♦X ∧ µY(. . . )] ⟨s, µY(P ∨ ♦Y)⟩
⟨t, ♦X⟩
⟨t, P ∨ ♦Y⟩
[t, P]
⟨t, ♦Y⟩
⟨t, Y⟩
⟨t, X⟩




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))
)