Information Technology Reference
In-Depth Information
M
may not be deterministic in the sense that for some
s
∈
S
M
and some
Note that
ʣ
there may be
more than
one
t
such that
s
a
a
t
.Intuitively this means that doing
a
on state
s
may result in different states due to some external factors which are not
modelled in
∈
→
.
The simplest procedure is a one-step atomic action
a
M
ʣ
, based on which more
complicated procedures are constructed as regular expressions:
ˀ
::=
a | ˀ
;
ˀ | ˀ
+
ˀ | ˀ
∗
∈
where
a
ʣ
.Intuitively, ; is the sequential composition, + is the non-deterministic
choice, and
∗
is the iteration operation. Let
ʠ
Σ
denote the set of all regular expressions
based on
ʣ
. The set of action sequences denoted by a regular expression
ˀ
(notation:
L
(
ˀ
)) is defined as follows:
L
∈
(
a
)=
{
a
}
(
ˀ
;
ˀ
)=
(
ˀ
)
L
{
wv
|
w
∈L
(
ˀ
) and
v
∈L
}
(
ˀ
+
ˀ
)=
(
ˀ
)
L
L
(
ˀ
)
∪L
}∪
n>
0
(
(
ˀ
∗
)=
L
{
L
(
ˀ
;
···
;
ˀ
))
n
where
is the empty sequence. In the sequel, we abuse the notation by writing
w
∈
ˀ
(
ˀ
).
We use the languageofPDL to describe the procedures encoded in a Kripke model:
ˆ
::=
ˀ
for
for
w
∈L
(
ˀ
) and writing
ˀ
ↆ
L
(
ˀ
)
ↆL
|
p
|¬
ˆ
|
ˆ
∧
ˆ
|
ˀ
ˆ
where
ˀ
ˆ
formulas are interpreted on pointed Kripke model
M
,s
as follows (cf. e.g.,
[7]):
there exists a
t
such that
s
w
M
,s
ˀ
ˆ
⃒⃐
→
t
for some
w
∈
ˀ
and
t
ˆ
We s a y
s
0
,s
1
,...,s
n
is an
execution
of
ˀ
if there exist
w
=
a
1
,a
2
,...,a
n
∈
ˀ
such
a
k
+1
→
that
s
k
ˆ
is trueat
s
iff there is an
execution of
ˀ
from
s
to a
ˆ
-state
, i.e., a state where
ˆ
holds.
Now, we formalize a piece of imperfect procedure information as a Hoare-like triple
s
k
+1
for 0
≤
k<n
. In another word,
ˀ
where
ˆ
and
ˈ
are PDL formulas and
X
is one of
ˀ
∃
or
ˀ
∀
where
ˀ
ʠ
Σ
.
ˆ
and
ˈ
denote the
precondition
(initial states) and the
postcondition
(goal states) of the
procedure respectively, and
ˀ
denotes the procedure quantified by
ˆ, X, ˈ
∈
∃
or
∀
.Intuitively,
the quantifiers work as follows:
-
ˆ, ˀ
∃
,ˈ
says that if
ˆ
holds then there
exists
an execution of
ˀ
which can make
ˈ
true, e.g., “One of these two buses will get you to the university from home.”
ˆ, ˀ
∀
,ˈ
says that if
ˆ
holds then
all
the executions of
ˀ
will make sure
ˈ
,e.g.,
“All the buses departing here will get you to the university.”
The
correctness
of a piece of information
-
ˆ, X, ˈ
is defined below, given a Kripke
model
M
:
t
:
t
w
ˆ, ˀ
∃
,ˈ
t
and
t
-
is correct iff (
∀
t
ˆ
,
∃
w
∈
ˀ
∃
→
ˈ
)iff
M
ˆ
→
ˀ
ˈ
t
:if
t
w
ˆ, ˀ
∀
,ˈ
t
then
t
-
is correct iff (
∀
t
ˆ
,
∀
w
∈
ˀ
∀
→
ˈ
)iff
M
ˆ
→
[
ˀ
]
ˈ