Information Technology Reference
In-Depth Information
relations between states, such as the epistemic temporal models in [10,4,11,15] and the
models of imperfect information games in game theory (cf. e.g., [9]). In such epistemic
logical frameworks, a proposition is known on a state if it is true on all the possible
states linked with the current state by the epistemic relation.
However, explicitly representing possibilities as in the usual epistemic logical frame-
works leads to the problem of state space explosion even in very simple case, if there is
considerable ignorance. For example, if we have no idea how those four cities are con-
nected by possibly four transportation methods (e.g., train, bus, flight, boat), then there
are at least (2
4
∗
3
)
4
=2
48
>
10
14
possible maps, which is in the order of the number
of cells in a human body or the number of neuronal connections in a human brain. It is
clear that in reality we do not gothrough all these possibilities in ourmindtoacquire
knowledge. This leads to our first research question:
Can we have a compact alternative model of epistemic logic of procedures
without explicitly representing all the possibilities?
Moreover, it is important to incorporate new (imperfect) information about proce-
dures into the current model which allows us to incrementally build up the model even
from scratch. The new information may be given in a syntactic form which uses implicit
quantifiers, such as '
there is
abus going from
A
to
either
B
or
C
,but I am not quite
sure which due to the recent changeofroutes. On the other hand, from both
B
or
C
you
should be able to reach
D
by
some
public transportation.' The imperfect information
may also be given by a complicated procedure which is not just one-step, e.g., 'taking
abus then a train will get you home'. However, the semantic way of incorporating new
information is usually done by essentially
eliminating
inconsistent possibilities accord-
ing to the new information in epistemic frameworks such as dynamic epistemic logic
[2], which again assumes that all the possibilities are represented in the model. Thus
the following question is another challenge:
How to incorporate new proceduralinformation semantically inanincremen-
talfashion?
The technical contribution of this paper is a new semantics-driven epistemic logical
framework aiming at solving the above questions. Note that we may alternatively rep-
resent all the imperfect information syntactically but in the case of procedural informa-
tion, the graphic models are more natural and compact for very complicated procedural
information between states. Moreover, doing model checking is in general computa-
tionally more efficient than theorem proving. In the rest of this introduction, we will
explain our main ideas.
Main Ideas
To handle the first question, we need a way to encode possibilities in a compact and
implicit way. Our approach is inspired by the 3-valued abstraction technique in model
checking (see [5] for an overview). To handle the problem of state space explosion in
model checking, the abstraction technique makes a Kripke model smaller by abstracting
away some information. Clearly, the smaller abstract model may not preserve the truth
