Information Technology Reference
In-Depth Information
2
Preliminaries
This section recalls some basic concepts from [17]. We work on the single agent case,
buttheresults obtained can be easily extended to multi-agent scenarios.
Throughout this paper, let
Prop
beacountable set of atomic propositions. The lan-
guage
L
EL
extends the classical propositional language with formulas of the form
˕
,
read as “the agent knows that
˕
”. Formally,
˕
::
=
p
|¬˕|˕∧ˈ|
˕
with
p
∈
Prop
. Other propositional connectives (
∨,ₒ
and
ₔ
) are defined as usual. The
dual of
.
A
monotone neighborhood frame
is a pair
is defined as
˕
:
=¬
¬˕
F =
(
W
,˄
)where
W
∅
is the domain, a
set of possible worlds, and
(
W
)) is a neighborhood function satisfying the
following monotonicity condition: for all
˄
:
W
ₒ℘
(
℘
w∈
W
and all
X
,
Y
ↆ
W
,
X
∈˄
(
w
)and
X
ↆ
Y
implies
Y
∈˄
(
w
). A
monotone neighborhood model
(
MNM
)
M=
(
F,
V
) is a monotone
neighborhood frame
F
together with a valuation function
V
:
Prop
ₒ ℘
(
W
). Given a
M=
(
W
,˄,
V
)anda
L
EL
-formula
˕
, the notion of
˕
being trueatastate
w
in the model
M
(written
M,w|=˕
) is defined inductively as follows:
M,w|=
p
i
ffw∈
V
(
p
),
M,w|=˕∧ˈ
i
ffM,w|=˕
and
M,w|=ˈ
,
M,w|=¬˕
i
ffM,w|=˕
,
M,w|=
˕
i
ff ˕
M
∈˄
(
w
).
˕
M
:
={
∈
|M,
|=˕}
˕
M
M
where
u
W
u
is the truth set of
in
.Since
is a
MNM
,the
satisfaction clause for
can be equivalently rewritten as follows:
M,w|=
˕
i
ff
X
ↆ ˕
M
for some
X
∈˄
(
w
).
The language
L
PAL
extends
L
EL
with the public announcement operator [
˕
], allow-
ing the construction of formulas of the form [
˕
]
ˈ
, read as “
ˈ
is trueafterthepublic
announcement of
.) For the semantic interpretation, we re-
call the intersection and subset semantics of [17].
˕
”. (Define
˕ˈ
:
=¬
[
˕
]
¬ˈ
M =
,˄,
ↆ
Definition 1.
Let
(
W
V
)
be a MNM. For any non-empty U
W, definethe
function V
U
ₒ
Uby V
U
(
p
):
=
∩
∈
:
Prop
V
(
p
)
Uforeach p
Prop
.
M
M
∩
U
=
,˄
∩
U
,
V
U
)
,isgiven by
-
The
intersection submodel
of
induced by U,
(
U
˄
∩
U
(
u
):
={
P
∩
U
|
P
∈˄
(
u
)
}
,foreveryu
∈
U.
M
ↆ
U
,˄
ↆ
U
V
U
)
,isgiven by
˄
ↆ
U
(
u
):
-
The
subset submodel
of
M
induced by U,
=
(
U
,
=
{
P
∈˄
(
u
)
|
P
ↆ
U
}
,foreveryu
∈
U.
M
∩
U
M
ↆ
U
,asshownin[17].
If
M
is monotone, then so are
and
L
PAL
, the notion of a formula being
true at a state of a model extends that for formulas in
Given a
MNM
M =
(
W
,˄,
V
), formulas
˕,ˈ
in
L
EL
with the following clauses:
M
∩˕
,w|=
∩
ˈ
-
M,w|=
∩
[
˕
]
ˈ
i
ffM,w|=
∩
˕
implies
,
M
ↆ˕
,w|=
ↆ
ˈ
-
M,w|=
ↆ
[
˕
]
ˈ
i
ffM,w|=
ↆ
˕
implies
;
