Action Theory Revision In Dynamic Logic
This document was uploaded by user and they confirmed that they have the permission to share it. If you are author or own the copyright of this book, please report to us by using this DMCA report form. Report DMCA
Overview
Download & View Action Theory Revision In Dynamic Logic as PDF for free.
More details
- Words: 3,932
- Pages: 68
Action Theory Revision in Dynamic Logic Ivan Jos´ e Varzinczak Knowledge Systems Group Meraka Institute CSIR Pretoria, South Africa
NMR’2008
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
1 / 23
Motivation
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
Knowledge Base ‘A coffee is a hot drink’ ‘With a token I can buy coffee’ ‘Without a token I cannot buy’ ‘After buying I have a hot drink’ ...
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
Observations ‘Only coffee on the machine’ ‘After buying, I lose my token’ ‘Coffee is for free’
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
Observations ‘Only coffee on the machine’ ‘After buying, I lose my token’ ‘Coffee is for free’
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
k, t, c, h
b k, t, ¬c, h b
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation b
b
¬k, ¬t, c, h k, ¬t, c, h b b b b
k, t, c, h
b
b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Outline Preliminaries Action Theories in Dynamic Logic
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
3 / 23
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
3 / 23
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
3 / 23
Preliminaries
Action Theories in Dynamic Logic
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
4 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics
◮
Expressive
◮
Decidable
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics ◮
Possible worlds models
◮
Expressive
◮
Decidable
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics ◮
◮
Expressive ◮
◮
Possible worlds models Actions, state constraints, nondeterminism
Decidable
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics ◮
◮
Expressive ◮
◮
Possible worlds models Actions, state constraints, nondeterminism
Decidable ◮
exptime or pspace-complete, though
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Possible worlds semantics: Transition Systems M = hW , R i ◮
W : possible worlds
◮
R : accessibility relation p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
6 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Describing Laws
In RAA: 3 types of laws ◮
Static Laws: ϕ ◮
Ex.: p1 ∨ p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
7 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Describing Laws
In RAA: 3 types of laws ◮
Static Laws: ϕ ◮
◮
Ex.: p1 ∨ p2
Executability Laws: ϕ → hai⊤ ◮
Ex.: p2 → ha2 i⊤
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
7 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Describing Laws
In RAA: 3 types of laws ◮
Static Laws: ϕ ◮
◮
Executability Laws: ϕ → hai⊤ ◮
◮
Ex.: p1 ∨ p2
Ex.: p2 → ha2 i⊤
Effect Laws: ϕ → [a]ψ ◮
Ex.: p1 → [a1 ]p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
7 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2 → ha2 i⊤
◮
¬p1 → ha1 i⊤
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
"
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2 → ha2 i⊤
◮
¬p1 → ha1 i⊤
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
"
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2 → ha2 i⊤
◮
¬p1 → ha1 i⊤
"
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
"
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2
◮
¬p1 → ha1 i⊤
" → ha i⊤ " 2
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
◮
Action Theory Revision
"
◮
" p → ha i⊤ " ¬p → ha i⊤ % 2
2
1
1
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic In our exemple ◮
Static Law:
◮
coffee → hot
◮
Executability Law:
◮
token → hbuyi⊤
◮
Effect Law:
◮
¬coffee → [buy]coffee
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
9 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic In our exemple ◮
Static Law:
◮
coffee → hot
◮
Executability Law:
◮
token → hbuyi⊤
◮
Effect Law:
◮
¬coffee → [buy]coffee
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
9 / 23
Revision of Laws
Semantics of Revision
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
10 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by laws ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by hot → coffee ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by hot → coffee ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by hot → coffee ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by laws ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by token → [buy]¬token ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by token → [buy]¬token ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by token → [buy]¬token ¬k, ¬t, c, h
k, ¬t, c, h b
k, t, c, h
b k, t, ¬c, h b
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by laws ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by ¬token → hbuyi⊤ ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by ¬token → hbuyi⊤ ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b
b
b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision b
Revision by ¬token → hbuyi⊤ b
¬k, ¬t, c, h k, ¬t, c, h b b b b
k, t, c, h
b
b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Principles of Theory Change (Dalal, 1988) ◮
Irrelevance of Syntax
◮
Maintenance of Consistency
◮
Primacy of New Information
◮
Persistence of Prior Knowledge
◮
Fairness
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
12 / 23
Revision of Laws
Semantics of Revision
Principles of Theory Change (Dalal, 1988) ◮
Irrelevance of Syntax
◮
Maintenance of Consistency
◮
Primacy of New Information
◮
Persistence of Prior Knowledge
◮
Fairness
Ivan Jos´ e Varzinczak (KSG - Meraka)
+−
" " " "
Action Theory Revision
NMR’2008
12 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models ◮
Distance between models ◮ ◮
Prefer models closest to the original one Hamming/Dalal distance, etc
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
13 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models ◮
Distance between models ◮ ◮
◮
Prefer models closest to the original one Hamming/Dalal distance, etc
Distance dependent on the type of law to make valid ◮ ◮
Static law: look at the set of possible states (worlds) Action laws: look at the set of arrows
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
13 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models ◮
Distance between models ◮ ◮
◮
Prefer models closest to the original one Hamming/Dalal distance, etc
Distance dependent on the type of law to make valid ◮ ◮
Static law: look at the set of possible states (worlds) Action laws: look at the set of arrows
Definition Let M = hW , R i. M ′ = hW ′ , R ′ i is as close to M as M ′′ = hW ′′ , R ′′ i iff ˙ ′ ⊆ W −W ˙ ′′ ◮ either W −W ˙ ′ = W −W ˙ ′′ and R −R ˙ ′ ⊆ R −R ˙ ′′ ◮ or W −W Notation: M ′ M M ′′ Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
13 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ
Definition Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ⋆ iff: ◮
W ′ = (W \ val(¬ϕ)) ∪ val(ϕ)
◮
R′ ⊆ R
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
14 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ
Definition Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ⋆ iff: ◮
W ′ = (W \ val(¬ϕ)) ∪ val(ϕ)
◮
R′ ⊆ R
Definition revise(M , ϕ) =
S
min{Mϕ⋆ , M }
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
14 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by hot → coffee
¬k, ¬t, c, h
k, ¬t, c, h
¬k, ¬t, c, h
b b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Ivan Jos´ e Varzinczak (KSG - Meraka)
k, ¬t, c, h
¬k, t, c, h
b
M
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Action Theory Revision
NMR’2008
15 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → [a]ψ
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→[a]ψ iff: ◮
W′ = W
◮
R′ ⊆ R
◮
If (w , w ′ ) ∈ R \ R ′ , then |=w ϕ
◮
|= ϕ → [a]ψ
M
M′
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
16 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → [a]ψ
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→[a]ψ iff: ◮
W′ = W
◮
R′ ⊆ R
◮
If (w , w ′ ) ∈ R \ R ′ , then |=w ϕ
◮
|= ϕ → [a]ψ
M
M′
Definition revise(M , ϕ → [a]ψ) =
Ivan Jos´ e Varzinczak (KSG - Meraka)
S
⋆ min{Mϕ→[a]ψ , M }
Action Theory Revision
NMR’2008
16 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by token → [buy]¬token
¬k, ¬t, c, h
k, ¬t, c, h b
k, t, c, h
¬k, ¬t, c, h
k, ¬t, c, h
b k, t, ¬c, h b
M
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
k, t, c, h
k, t, ¬c, h
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Action Theory Revision
NMR’2008
17 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → hai⊤
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→hai⊤ iff: ◮
W′ = W
◮
R ⊆ R′
◮
If (w , w ′ ) ∈ R ′ \ R , then w ′ ∈ RelTarget(w , ¬(ϕ → [a]⊥))
◮
|= ϕ → hai⊤
M′
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
18 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → hai⊤
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→hai⊤ iff: ◮
W′ = W
◮
R ⊆ R′
◮
If (w , w ′ ) ∈ R ′ \ R , then w ′ ∈ RelTarget(w , ¬(ϕ → [a]⊥))
◮
|= ϕ → hai⊤
M′
Definition revise(M , ϕ → hai⊤) =
Ivan Jos´ e Varzinczak (KSG - Meraka)
S
⋆ min{Mϕ→hai⊤ , M }
Action Theory Revision
NMR’2008
18 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ¬token → hbuyi⊤ b
b
b
b
¬k, ¬t, c, h k, ¬t, c, h b b b
¬k, ¬t, c, h k, ¬t, c, h b b b b b b b b k, t, c, h k, t, ¬c, h k, t, c, h k, t, ¬c, h b Mb b b b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
19 / 23
Revision of Laws
Algorithms
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
20 / 23
Revision of Laws
Algorithms
Quick look: Correctness of the Algorithms ◮
T an action theory
◮
Φ a law
We have defined algorithms that revise T by Φ, giving T ′
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
21 / 23
Revision of Laws
Algorithms
Quick look: Correctness of the Algorithms ◮
T an action theory
◮
Φ a law
We have defined algorithms that revise T by Φ, giving T ′ ◮
ϕ a static law
◮
S ⊆ T set of static laws in T
Definition (Herzig & Varzinczak, AiML 2005) T is modular iff for every static law ϕ, if T |=PDLϕ, then S |=CPLϕ
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
21 / 23
Revision of Laws
Algorithms
Quick look: Correctness of the Algorithms ◮
T an action theory
◮
Φ a law
We have defined algorithms that revise T by Φ, giving T ′ ◮
ϕ a static law
◮
S ⊆ T set of static laws in T
Definition (Herzig & Varzinczak, AiML 2005) T is modular iff for every static law ϕ, if T |=PDLϕ, then S |=CPLϕ
Theorem Under modularity, the algorithms are correct w.r.t. our semantics
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
21 / 23
Conclusion
Conclusion Contribution ◮
Semantics for action theory revision ◮ ◮
Distance between models Minimal change
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
22 / 23
Conclusion
Conclusion Contribution ◮
Semantics for action theory revision ◮ ◮
◮
Distance between models Minimal change
Syntactic operators (algorithms) ◮
Correct w.r.t. the semantics
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
22 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
Invalidating formulas in a model (see talk at KR’08)
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
◮
Invalidating formulas in a model (see talk at KR’08)
Postulates for action theory revision
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
Invalidating formulas in a model (see talk at KR’08)
◮
Postulates for action theory revision
◮
Revision of general formulas ◮
not only ϕ, ϕ → hai⊤, ϕ → [a]ψ
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
Invalidating formulas in a model (see talk at KR’08)
◮
Postulates for action theory revision
◮
Revision of general formulas ◮
◮
not only ϕ, ϕ → hai⊤, ϕ → [a]ψ
Applications in Description Logics ◮
ontology evolution/debugging
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
NMR’2008
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
1 / 23
Motivation
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
Knowledge Base ‘A coffee is a hot drink’ ‘With a token I can buy coffee’ ‘Without a token I cannot buy’ ‘After buying I have a hot drink’ ...
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
Observations ‘Only coffee on the machine’ ‘After buying, I lose my token’ ‘Coffee is for free’
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
Observations ‘Only coffee on the machine’ ‘After buying, I lose my token’ ‘Coffee is for free’
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
k, t, c, h
b k, t, ¬c, h b
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Motivation b
b
¬k, ¬t, c, h k, ¬t, c, h b b b b
k, t, c, h
b
b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Need for change the laws about the behavior of actions
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
2 / 23
Outline Preliminaries Action Theories in Dynamic Logic
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
3 / 23
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
3 / 23
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
3 / 23
Preliminaries
Action Theories in Dynamic Logic
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
4 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics
◮
Expressive
◮
Decidable
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics ◮
Possible worlds models
◮
Expressive
◮
Decidable
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics ◮
◮
Expressive ◮
◮
Possible worlds models Actions, state constraints, nondeterminism
Decidable
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Dynamic Logic ◮
Well defined semantics ◮
◮
Expressive ◮
◮
Possible worlds models Actions, state constraints, nondeterminism
Decidable ◮
exptime or pspace-complete, though
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
5 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Possible worlds semantics: Transition Systems M = hW , R i ◮
W : possible worlds
◮
R : accessibility relation p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
6 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Describing Laws
In RAA: 3 types of laws ◮
Static Laws: ϕ ◮
Ex.: p1 ∨ p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
7 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Describing Laws
In RAA: 3 types of laws ◮
Static Laws: ϕ ◮
◮
Ex.: p1 ∨ p2
Executability Laws: ϕ → hai⊤ ◮
Ex.: p2 → ha2 i⊤
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
7 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Describing Laws
In RAA: 3 types of laws ◮
Static Laws: ϕ ◮
◮
Executability Laws: ϕ → hai⊤ ◮
◮
Ex.: p1 ∨ p2
Ex.: p2 → ha2 i⊤
Effect Laws: ϕ → [a]ψ ◮
Ex.: p1 → [a1 ]p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
7 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2 → ha2 i⊤
◮
¬p1 → ha1 i⊤
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
"
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2 → ha2 i⊤
◮
¬p1 → ha1 i⊤
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
"
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2 → ha2 i⊤
◮
¬p1 → ha1 i⊤
"
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
"
◮
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
p2
◮
¬p1 → ha1 i⊤
" → ha i⊤ " 2
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic Formulas that hold in M p1 , ¬p2 M :
a2
a1
p1 , p2
a2
a1
p1 ∨ p2
◮
p1 → [a1 ]p2
◮
¬p1 , p2
Ivan Jos´ e Varzinczak (KSG - Meraka)
◮
Action Theory Revision
"
◮
" p → ha i⊤ " ¬p → ha i⊤ % 2
2
1
1
NMR’2008
8 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic In our exemple ◮
Static Law:
◮
coffee → hot
◮
Executability Law:
◮
token → hbuyi⊤
◮
Effect Law:
◮
¬coffee → [buy]coffee
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
9 / 23
Preliminaries
Action Theories in Dynamic Logic
Action Theories in Dynamic Logic In our exemple ◮
Static Law:
◮
coffee → hot
◮
Executability Law:
◮
token → hbuyi⊤
◮
Effect Law:
◮
¬coffee → [buy]coffee
¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
9 / 23
Revision of Laws
Semantics of Revision
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
10 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by laws ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by hot → coffee ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by hot → coffee ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by hot → coffee ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by laws ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by token → [buy]¬token ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by token → [buy]¬token ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by token → [buy]¬token ¬k, ¬t, c, h
k, ¬t, c, h b
k, t, c, h
b k, t, ¬c, h b
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by laws ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by ¬token → hbuyi⊤ ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision Revision by ¬token → hbuyi⊤ ¬k, ¬t, c, h
k, ¬t, c, h b
b
k, t, c, h
b
b
b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Intuitions About Model Revision b
Revision by ¬token → hbuyi⊤ b
¬k, ¬t, c, h k, ¬t, c, h b b b b
k, t, c, h
b
b
k, t, ¬c, h b
b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
11 / 23
Revision of Laws
Semantics of Revision
Principles of Theory Change (Dalal, 1988) ◮
Irrelevance of Syntax
◮
Maintenance of Consistency
◮
Primacy of New Information
◮
Persistence of Prior Knowledge
◮
Fairness
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
12 / 23
Revision of Laws
Semantics of Revision
Principles of Theory Change (Dalal, 1988) ◮
Irrelevance of Syntax
◮
Maintenance of Consistency
◮
Primacy of New Information
◮
Persistence of Prior Knowledge
◮
Fairness
Ivan Jos´ e Varzinczak (KSG - Meraka)
+−
" " " "
Action Theory Revision
NMR’2008
12 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models ◮
Distance between models ◮ ◮
Prefer models closest to the original one Hamming/Dalal distance, etc
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
13 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models ◮
Distance between models ◮ ◮
◮
Prefer models closest to the original one Hamming/Dalal distance, etc
Distance dependent on the type of law to make valid ◮ ◮
Static law: look at the set of possible states (worlds) Action laws: look at the set of arrows
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
13 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models ◮
Distance between models ◮ ◮
◮
Prefer models closest to the original one Hamming/Dalal distance, etc
Distance dependent on the type of law to make valid ◮ ◮
Static law: look at the set of possible states (worlds) Action laws: look at the set of arrows
Definition Let M = hW , R i. M ′ = hW ′ , R ′ i is as close to M as M ′′ = hW ′′ , R ′′ i iff ˙ ′ ⊆ W −W ˙ ′′ ◮ either W −W ˙ ′ = W −W ˙ ′′ and R −R ˙ ′ ⊆ R −R ˙ ′′ ◮ or W −W Notation: M ′ M M ′′ Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
13 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ
Definition Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ⋆ iff: ◮
W ′ = (W \ val(¬ϕ)) ∪ val(ϕ)
◮
R′ ⊆ R
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
14 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ
Definition Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ⋆ iff: ◮
W ′ = (W \ val(¬ϕ)) ∪ val(ϕ)
◮
R′ ⊆ R
Definition revise(M , ϕ) =
S
min{Mϕ⋆ , M }
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
14 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by hot → coffee
¬k, ¬t, c, h
k, ¬t, c, h
¬k, ¬t, c, h
b b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Ivan Jos´ e Varzinczak (KSG - Meraka)
k, ¬t, c, h
¬k, t, c, h
b
M
b
k, t, c, h
b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h
Action Theory Revision
NMR’2008
15 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → [a]ψ
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→[a]ψ iff: ◮
W′ = W
◮
R′ ⊆ R
◮
If (w , w ′ ) ∈ R \ R ′ , then |=w ϕ
◮
|= ϕ → [a]ψ
M
M′
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
16 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → [a]ψ
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→[a]ψ iff: ◮
W′ = W
◮
R′ ⊆ R
◮
If (w , w ′ ) ∈ R \ R ′ , then |=w ϕ
◮
|= ϕ → [a]ψ
M
M′
Definition revise(M , ϕ → [a]ψ) =
Ivan Jos´ e Varzinczak (KSG - Meraka)
S
⋆ min{Mϕ→[a]ψ , M }
Action Theory Revision
NMR’2008
16 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by token → [buy]¬token
¬k, ¬t, c, h
k, ¬t, c, h b
k, t, c, h
¬k, ¬t, c, h
k, ¬t, c, h
b k, t, ¬c, h b
M
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
k, t, c, h
k, t, ¬c, h
k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Action Theory Revision
NMR’2008
17 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → hai⊤
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→hai⊤ iff: ◮
W′ = W
◮
R ⊆ R′
◮
If (w , w ′ ) ∈ R ′ \ R , then w ′ ∈ RelTarget(w , ¬(ϕ → [a]⊥))
◮
|= ϕ → hai⊤
M′
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
18 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ϕ → hai⊤
Definition ⋆ Let M = hW , R i. M ′ = hW ′ , R ′ i ∈ Mϕ→hai⊤ iff: ◮
W′ = W
◮
R ⊆ R′
◮
If (w , w ′ ) ∈ R ′ \ R , then w ′ ∈ RelTarget(w , ¬(ϕ → [a]⊥))
◮
|= ϕ → hai⊤
M′
Definition revise(M , ϕ → hai⊤) =
Ivan Jos´ e Varzinczak (KSG - Meraka)
S
⋆ min{Mϕ→hai⊤ , M }
Action Theory Revision
NMR’2008
18 / 23
Revision of Laws
Semantics of Revision
Minimal Change Choosing models: revising by ¬token → hbuyi⊤ b
b
b
b
¬k, ¬t, c, h k, ¬t, c, h b b b
¬k, ¬t, c, h k, ¬t, c, h b b b b b b b b k, t, c, h k, t, ¬c, h k, t, c, h k, t, ¬c, h b Mb b b b b k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h k, ¬t, ¬c, ¬h k, t, ¬c, ¬h k, ¬t, ¬c, h
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
19 / 23
Revision of Laws
Algorithms
Outline Preliminaries Action Theories in Dynamic Logic
Revision of Laws Semantics of Revision Algorithms
Conclusion
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
20 / 23
Revision of Laws
Algorithms
Quick look: Correctness of the Algorithms ◮
T an action theory
◮
Φ a law
We have defined algorithms that revise T by Φ, giving T ′
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
21 / 23
Revision of Laws
Algorithms
Quick look: Correctness of the Algorithms ◮
T an action theory
◮
Φ a law
We have defined algorithms that revise T by Φ, giving T ′ ◮
ϕ a static law
◮
S ⊆ T set of static laws in T
Definition (Herzig & Varzinczak, AiML 2005) T is modular iff for every static law ϕ, if T |=PDLϕ, then S |=CPLϕ
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
21 / 23
Revision of Laws
Algorithms
Quick look: Correctness of the Algorithms ◮
T an action theory
◮
Φ a law
We have defined algorithms that revise T by Φ, giving T ′ ◮
ϕ a static law
◮
S ⊆ T set of static laws in T
Definition (Herzig & Varzinczak, AiML 2005) T is modular iff for every static law ϕ, if T |=PDLϕ, then S |=CPLϕ
Theorem Under modularity, the algorithms are correct w.r.t. our semantics
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
21 / 23
Conclusion
Conclusion Contribution ◮
Semantics for action theory revision ◮ ◮
Distance between models Minimal change
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
22 / 23
Conclusion
Conclusion Contribution ◮
Semantics for action theory revision ◮ ◮
◮
Distance between models Minimal change
Syntactic operators (algorithms) ◮
Correct w.r.t. the semantics
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
22 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
Invalidating formulas in a model (see talk at KR’08)
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
◮
Invalidating formulas in a model (see talk at KR’08)
Postulates for action theory revision
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
Invalidating formulas in a model (see talk at KR’08)
◮
Postulates for action theory revision
◮
Revision of general formulas ◮
not only ϕ, ϕ → hai⊤, ϕ → [a]ψ
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Conclusion
Conclusion Ongoing research and future work ◮
Action theory contraction ◮
Invalidating formulas in a model (see talk at KR’08)
◮
Postulates for action theory revision
◮
Revision of general formulas ◮
◮
not only ϕ, ϕ → hai⊤, ϕ → [a]ψ
Applications in Description Logics ◮
ontology evolution/debugging
Ivan Jos´ e Varzinczak (KSG - Meraka)
Action Theory Revision
NMR’2008
23 / 23
Related Documents
Action Theory Revision In Dynamic Logic
October 2019 6
Action Theory Revision In Dynamic Logic
October 2019 7
Dynamic Logic Circuits 14
November 2019 18
Dynamic Comp Action Applications
June 2020 3
Theory Of Reasoned Action
June 2020 11
Theory Of Reasoned Action
May 2020 4More Documents from ""
Freindship
October 2019 124
Industria Iso099.docx
November 2019 83
S2.pdf
December 2019 90
Humn1.docx
December 2019 93