Information Technology Reference
In-Depth Information
Proposition 4.
INV
:(
p
→
Kp
)
∧
¬
p
→
K
¬
p
)
is valid.
(
To completely axiomatize the logic, it is also important to have axioms controlling the
interactions between
K
and [
a
]. Here we observe that the axiom of
perfect recall
(
PR
)
is valid:
K
[
a
]
ˆ
[
a
]
Kˆ
while the converse (
nolearning
) is invalid.
3
→
Proposition 5.
PR
:
K
[
a
]
ˆ
→
[
a
]
Kˆ
is valid.
We l e ave i t f o r future work whether
PR
,
INV
,
DIST
∧,
DIST
∨
,
DIST
,
T
,
5
,
4
on top of
a propositional calculusareenough to completely axiomatize EAL over simple hyper
frames.
3.2
Models with Arbitrary Procedural Information
In this subsection, we consider arbitrary procedural information. Intuitively, the correct
information
ˆ, ˀ
∀
,ˈ
ˆ, ˀ
∃
,ˈ
(
) can be incorporated by adding to the model
M
a
transition labelled by
ˀ
∀
(
ˀ
∃
) from
and this
leads to the definition of unrestricted hyper models (recall that
ʠ
Σ
is the set of regular
expressions based on
ʣ
):
{M
,s
|
s
ˆ
}
to
{M
,t
|
t
ˈ
}
Definition 5 (Hyper Model).
Anhyper model is a tuple
(
S,
→
,
→
∃
,
→
∀
,V
)
where:
-
(
S,
→
,V
)
is a Kripke model
2
S
2
S
is a labelled binary relation fromaset of states to a set of
-
→
∃
ↆ
×
ʠ
Σ
×
states.
2
S
2
S
is a labelled binary relation fromaset of states to a set of
-
→
∀
ↆ
×
ʠ
Σ
×
states.
-
for all
T,T
ↆ
ˀ
→
∃
T
implies thatforall
t
S
:
T
∈
T
there exists
w
∈
ˀ
and
T
such that
t
w
t
∈
t
.
→
ˀ
→
∀
T
implies thatforall
t
ˀ
:
t
w
-
for all
T,T
ↆ
t
implies
S
:
T
∈
T
all
w
∈
→
t
∈
T
.
Again, the last two conditions guarantee that the information incorporated in the models
are correct. The class of simple hyper models can be viewed as a subclass of hyper
models, where the transitions are all in the shapes of
a
→
∃
T
and
a
→
∀
T
.
{
s
}
{
s
}
Now we can consider the full EPDL language.
Definition 6 (Epistemic PDL).
Givenacountable set of
propositional variables
P
, a
finite set of
action symbols
ʣ
,theformulasofEPDL language are defined by:
ˆ
::=
|
p
|¬
ˆ
|
(
ˆ
∧
ˆ
)
|
Kˆ
|
ˀ
ˆ
ˀ
∗
ˀ
::=
a
|
ˀ
;
ˀ
|
ˀ
+
ˀ
|
where
a
∈
ʣ
and
p
∈
P
.
3
Versions of these axioms appear in temporal epistemic logic and dynamic epistemic logic (cf.
[4,14]).
