Information Technology Reference
In-Depth Information
Kˆ
and [
a
]
ˆ
as the abbreviations of
↥
,
ˆ
∨
ˈ
,
ˆ
→
ˈ
,
¬
As usual, we define
,
¬
¬
ˆ
∧¬
ˈ
),
¬
ˆ
∨
ˈ
,
¬
K
¬
ˆ
and
¬
a
¬
ˆ
respectively.
(
Definition 4 (Semantics).
Thesemantics of EAL onasimple hyper model
M
=(
S,
→
,
,
→
∃
→
∀
,V
)
is given by the following satisfaction relationw.r.t. amode
x
∈{
0
,
,
♦
}
:
M,s
φ ⃔M,s
0
φ
M,s
x
p ⃔ p ∈ V
(
s
)
M,s
x
φ ∧ ˈ ⃔M,s
x
φ
and
M,s
x
ˈ
M,s
x
Kφ ⃔M,s
φ
⊨
M,s
0
φ
IF
x
=0
M,s
♦
φ
IF
x
=
M,s
φ
IF
x
=
♦
M,s
x
¬φ ⃔
⊩
⊨
⊩
∃t ∈ S
:
s
a
ₒ t
and
M,t
0
φ
IF
x
=0
∃T ↆ S
:
s
a
M,s
x
aφ ⃔
ₒ
∃
T
and
∀t ∈ T
:
M,t
φ
IF
x
=
∀T ↆ S
:
s
a
ₒ
∀
T
implies
∃t ∈ T
:
M,t
♦
φ
IF
x
=
♦
We say that
ˆ
is valid in
M
(
M
ˆ
)ifforany
s
∈
S
M
:
M
,s
ˆ
.
ˆ
is valid if for any
M
:
M
ˆ
.
Clearly, this clumsy-looking semanticsneedsagood explanation. First of all,
and
can
be viewed as
contexts
in evaluating the formulas. More precisely, 0 marks the factual
mode: evaluating formulas outside the scope of any knowledge operator, while
♦
are used as auxiliary semantics in order to define
(
0
). 0,
and
♦
and
♦
denote the
knowledge modes
with the following intentions:
-
ˆ
:theagent thinks that
ˆ
is
necessarily
true, i.e.,
ˆ
is truein
all
the actual
situations consistent with the procedural information that he has.
-
♦
ˆ
:theagent thinks that
ˆ
is
possibly
true, i.e.,
ˆ
is truein
some
of the actual
situations consistent with the procedural information that he has.
The alternations of
are triggered by negations: according to the agent, if
ˆ
is
necessarily true then it is not possible to be not true, and if it is possible to be not true
then it is not necessarily true. The clause for
Kˆ
says that the agent knows
ˆ
iff he
thinks
ˆ
is necessarily true. Careful readers may wonder about the fact that
♦
and
M
,s
0
p
♦
p
, which means that a basic proposition is
trueifftheagent thinks that it is necessarily trueifftheagent thinks that it is possibly
true. This is because we assume the agent does not have any uncertainty about the basic
propositions on the states. There is only uncertainty about the transitions (“
The agent
knows all the cities but does not knowhow theyare connected
”).
1
Note that the above semantics coincides with the standard possible world semantics
on formulas withoutthe
K
-operator. When evaluating epistemic formulas, things get
more complicated. Note that we have a non-standard semantics for negation, thusitis
worth working out the semantics for abbreviations, e.g.,
⃒⃐ M
,s
p
⃒⃐ M
,s
M
,s
x
ˆ
→
ˈ
may not be
1
Actually we can incorporate uncertainty about the basic propositions by adding over- and
under-approximations of the truth values of them. We leave it to future work.
