Information Technology Reference
In-Depth Information
actual transitions. In this section, we discuss some subtle issues about the semantics and
point outfurther directions.
First of all, we justify that hyper models are indeed compact representations of a col-
lection of Kripke models. On the one hand, each hyper model
M
can be unfolded into
a set (call it
Unf
(
)) of Kripke models over the same set of states on which the im-
perfect information given by
M
→
∀
transitions in the hyper model is correct, i.e.,
satisfying the last two conditions in the definition of hyper models. Based on Lemma 2,
we can easily show that the knowledge in any hyper model
→
∃
and
M
are truthfulto
Unf
(
M
),
and
M
encodes all the possibilities in
Unf
(
M
):
Proposition 6.
Fo r everyPDL formula
ˆ
andevery
s
in any hyper model
M
:
-
if
M
,s
Kˆ
then
N
,s
ˆ
for every
N∈
Unf
(
M
)
Kˆ
-
if
N
,s
ˆ
for some
N∈
Unf
(
M
)
then
M
,s
Note that even in very simple cases,
|
Unf
(
M
)
|
may be
exponential
in the size of the
hyper model and
ʣ
. For example, let
S
=
{s, t}
,
V
(
p
)=
t
,andlet
ˀ
Σ
be the 'sum' of
ˀ
Σ
→
∀
{
as the only transition has 2
|ʣ|
all actions in
ʣ
, then the hyper model with
{
s
}
t
}
epistemically possible Kripke models to realize all the
ˆ
ʔ
=
a∈ʔ
∧
b∈ʔ
¬
a
p
b
p
formulas at
s
for each
ʔ
ʣ
. If the hyper model does not provide any procedural
information (i.e., deleting the only transition) then
ↆ
=2
|S|·|ʣ|·|S|
.
On the other hand, we may ask: is every set of concrete models (over a given set of
states
S
) representable by a hyper model over
S
? Unfortunately, the answer is negative.
For example, take the set of two Kripke models over
S
=
|
Unf
(
M
)
|
a
→
b
→
{
s, t
}
:
s
t
and
s
t
.
Let
ˆ
=(
). It is clear that
Kˆ
is true w.r.t. this set
of models and state
s
. However, over
S
, no matter how the
a
∧ ¬
b
)
∨
(
b
∧ ¬
a
→
∃
transitions
are chosen, we cannot make sure
Kˆ
holds on
s
since it would imply the knowledge
of one of the disjunctions according to Proposition 3. The problem lies in the fact that
we treat disjunction in the scope of
K
as “knowing whether” due to the semantics for
Boolean connectives. We cannot really specify certain kinds of
inter-dependency
be-
tween the transitions. We may have a hyper model over
s
with the following transition
{s}
→
∀
and
a
→
b
→
{t}
are mutually exclusive
between
s
and
t
. One potential solution is to make the labels of the transitions more ex-
pressive to specify conditional information, butwesuspect a 'satisfactory' solution will
in turn introduce another kind of 'state-explosion' on the transitions in hyper models.
We need to find the balance between expressiveness and complexity.
Moreover, althoughthelogic validates the
T
axiom, which makes sure everything
we know is truthful, it is not very clear how much information we can 'know' by the
semantics of EPDL on the hyper models. It seems that by requiring more conditions on
the hyper model we may get more from the hyper models. Let us illustrate this in the
simple hyper models. Below lists some intuitive closure properties that we may impose
and their corresponding logical properties:
,but we cannot make sure
and
(
a
+
b
)
∃
(
s
a
ₒ
∀
T
1
and
s
a
ₒ
∀
T
2
) implies
s
a
ₒ
∀
T
1
∩ T
2
K
[
a
]
φ ∧ K
[
a
]
ˈ ₒ K
[
a
](
φ ∧ ˈ
)
(
s
a
ₒ
∀
T
1
and
s
a
ₒ
∃
T
2
) implies
s
a
ₒ
∃
T
1
∩ T
2
K
[
a
]
φ ∧ Kaˈ ₒ Ka
(
φ ∧ ˈ
)
for each
s
each
a
, there exists
T ↆ S
such that
s
a
ₒ
∀
T
K
[
a
]
