IA: Computational Logic
. 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 and T are bisimilar if, and only if,
S ⊧ φ ⇔ 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
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.
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
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 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 EXPTIME-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)
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
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.)
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))
)