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
ˆ
[ ˀ ] ˈ
 
Search WWH ::




Custom Search