Information Technology Reference
In-Depth Information
value of all the formulas in concern, butasuitable 3-valued semantics on abstractions
can make sure the following:
-
formulas that are true in the abstraction are also true in the original model
-
formulas that are false in the abstraction are also false in the original model
In our point of view, an abstraction can be indeed viewed as a compact representation
of potential concrete models which are consistent with the information represented in
the abstract model. The information of transitions in the abstract model is typically
encoded by two special kinds of transitions which are under- and over-approximations
of the ones in the actual model [13]. This inspired ustouse similar abstract transitions
to encode imperfect procedural information. The final source of inspiration is from [3,1]
where the approximations of the transitions are labelled by regular expressions and this
helps us in dealing with arbitrarily complicated procedural information expressed by
regular expressions.
Based on these ideas, we propose
hyper models
to encode the imperfect procedural
information, and an epistemic PDL defined on such models, with the following features:
-
Hyper models assemble possibilities in an implicit and compact way using abstract
transitions (labelled by regular expressions) but not epistemic accessibility rela-
tions.
-
They incorporate new information incrementally by
adding
new transitions.
-
The semantics of ourlanguage is defined on the hyper models
directly
,andthereis
no need to unpack the hyper models into numerous possible Kripke models.
-
The logic is still 2-valued and
all
the usual
S5
axioms are valid, but
not
the neces-
sitation rule which may cause logical omniscience.
Of course, there is also a price to pay: not all the collections of Kripke models are
representable by hyper models, to which we will come back in Section 4. In the rest
of the paper, we first formalize imperfect procedural information in Section 2, and then
introduce and discuss simple and full hyper models in Section 3. Finally we show that
hyper models are indeed compact representations of Kripke models and point outfuture
directions in Section 4.
2
Preliminaries
Kripke models are used to represent how states are connected by atomic actions:
Definition 1 (Kripke Model).
Givenaset of basic propositional letters
P
, and a set of
atomic action symbols
ʣ
, a Kripke model
M
over
P
and
ʣ
is a tuple
(
S,
→
,V
)
where:
-
S
is anon-empty set of states.
-
→ↆ
S
×
ʣ
×
S
is a binary relation over
S
labelled byaction symbols from
ʣ
.
2
P
assignstoeach state a setofbasic propositional letters.
-
V
:
S
→
a
→
w
→
We write
s
t
if
(
s, a, t
)
∈→
. Given
w
=
a
1
a
2
...a
n
we write
s
t
if there are
s
0
,s
1
,...,s
n
such that
s
0
=
s
and
s
n
=
t
and
s
k
a
k
→
s
k
+1
for all
0
≤
k<n
.
