Information Technology Reference
In-Depth Information
Let
λ
be a (finite or infinite) trace. We denote by
Pref
(
λ
) the set of finite
prefixes of
λ
. More generally, if
Tr
is a set of traces,
Pref
(
Tr
)=
λ∈Tr
Pref
(
λ
).
Let
u, v
(
A
∗
)
n
,
u
=(
x
1
,x
2
,...,x
n
)
,v
=(
y
1
,y
2
,...,y
n
). We denote by
∈
u
⊗
v
the
simple interleaving
of
u
and
v
defined as
u
⊗
v
=
x
1
y
1
x
2
y
2
...x
n
y
n
.
(
A
∗
)
n
,wedenoteby
U
If
U, V
⊂
⊗
V
the set:
U
⊗
V
=
{
u
⊗
v
|
u
∈
U, v
∈
V
}
.
(
A
∗
)
ω
, the definition of
U
V
is extended in a standard way.
The interleaving of two sequences
x, y
, denoted by
interl
(
x, y
)isthesetof
sequences:
If
U, V
⊂
⊗
{
x
1
y
1
x
2
y
2
...x
n
y
n
|
x
=
x
1
x
2
...x
n
,n
∈
N
,y
=
y
1
y
2
...y
n
,x
i
,y
i
∈
A
∗
}
.
This extends to sets of sequences:
interl
(
X, Y
)=
{interl
(
x, y
)
| x ∈ X, y ∈ Y }
.
Probabilistic Event System
The execution of a system is modeled by its set
Tr
of traces which are finite or
infinite sequences of atomic events from a set
E
. A particular atomic event
τ
is
distinguished which represents the halting of the system. For example, if
λ
is a
sequence of atomic events, it is useful to distinguish between “
λ
has occurred but
the system still executes”, and “
λ
has occurred and the system has stopped”.
The latter case is modeled by the event
λτ
. To unify the presentation, it is
convenient to use only infinite sequences, writing
λτ
ω
instead of
λτ
. Then, from
now on,
Tr
is a set of infinite sequences which do not contain any occurrence of
τ
except when they are of the form
λτ
ω
where
λ
contains no occurrence of
τ
.
The set of atomic events
E
is divided into two disjoint sets, the set
H
of high-
level atomic events and the set
L
of low-level ones. Depending on the situation,
the stop event
τ
can be considered as a low-level or a high-level event. In this
paper, we only consider the case when the low-level user can observe that the
system has stopped, i.e.,
τ
L
.
The set of traces
Tr
is equipped with a probability measure
µ
over the
σ
-
algebra generated by the cylinders
λE
ω
,
λ
∈
E
∗
, such that
Tr
is
µ
-measurable.
The measure
µ
(
X
) of a measurable set
X
is denoted as
Pr
µ
(
X
), or shortly
Pr
(
X
). Thus if we consider the infinite tree
T
built from
Tr
with edges labeled
by atomic events, each edge of the tree is equipped with a non-zero probability.
(We assume that every prefix of a trace in
Tr
has a non-zero probability).
Traditionally, an event is a measurable set in the theory of probabilities, so
to avoid confusion, the atomic events of the system will be called actions.
We use the customary notation for conditional probabilities: if
P
and
Q
are
two measurable events and
Pr
(
Q
)
∈
= 0, the conditional probability
Pr
(
P
|
Q
)is
Pr
(
P
Q
)
/Pr
(
Q
). Since we are interested only in traces of the system
S
we deal
only with conditional probabilities relative to
Tr
. Thus, for each measurable
event
X
we denote by
Pr
S
(
X
) the probability
Pr
(
X
∩
|
S
) (assuming
Pr
(
S
)
>
0).
Definition 1.
An event system S is a tuple
(
E, H, L,Tr ,µ
)
where E
=
H
L,
and H (resp. L) is the set of high-level (resp. low-level) actions, Tr is the set of
traces of the system, and µ is a probabilistic measure on Tr.
∪
We assume that only low-level actions are observable on the low-level, i.e.,
for a trace
λ
the projection
λ
|L
is observable by low-level users. More precisely,
a finite prefix of
λ
|L
is observable. Thus, from the observation of
u
L
∗
,the
∈
