Information Technology Reference
In-Depth Information
Representing Imperfect Information of Procedures
with Hyper Models
Yanjing Wa ng
Department of Philosophy, Peking University, Beijing, China
y.wang@pku.edu.cn
Abstract.
When reasoning about knowledge of procedures under imperfect in-
formation, the explicit representation of epistemic possibilities blows uptheS5-
like models of standard epistemic logic. To overcome this drawback, in this paper,
we propose a new logical framework based on compact models withoutepistemic
accessibility relations for reasoning about knowledge of procedures. Inspired by
the 3-valued abstraction method in model checking,weintroduce hyper models
which encode the imperfect procedural information. We give a highly non-trivial
2-valued semantics of epistemic dynamic logic on such models while validating
all the usual S5 axioms. Our approach is suitable for applications where procedu-
ral information is 'learned' incrementally, as demonstrated by variousexamples.
1
Introduction
Suppose there are four cities
A
,
B
,
C
,
D
which are connected by public transportation
as the following leftmost map shows (
b
for busand
t
→
→
for train):
A
t
B
b
A
t
t
B
b
A
b
t
B
b
A
t
B
b
b
b
b
b
t
b
t
t
t
t
D
C
D
C
D
C
D
C
We may view the map as a Kripke model and use various modal logics such as Propo-
sitional Dynamic Logic (PDL) [12] to describe routes or more complicated trip plans
from one city to others. Now suppose we are informed that
A
and
D
will also be con-
nected next year, but it is not clear whether it will be a bus line or a train connection or
even both. Then the new map can be any one of the three right-hand-side maps above.
Although the new information is
imperfect
, we still can
know
that city
D
will become
directly reachable from
A
since this is true in all the possible new maps, and it may be
possible
to reach
C
from
A
by train via
D
, since this is true in some possible maps.
As we have seen, imperfect information about the connectivity of the states intro-
duces uncertainty. To encode such uncertainty, two-dimensional Kripke models are
often used, which not only have labelled transitions but also epistemic accessibility
