Information Technology Reference
In-Depth Information
A node has the color of the edge ending in this node. The root is red.
Two red nodes
x
and
x
of
T
are
H-equivalent
if there exists an integer
n
such that the labels of the paths from the root to
x
and
x
are respectively
α
1
a
1
α
2
a
2
...α
n
a
n
and
α
1
b
1
α
2
b
2
...α
n
b
n
where
α
i
∈
H
∗
and
a
i
,b
i
∈
L
.
We also need to state an equivalence property on
L
. Two nodes
x
and
x
of
T
are
L-equivalent
if there exists an integer
n
such that the labels of the
paths from the root to
x
and
x
are respectively
α
1
a
1
α
2
a
2
...α
n−
1
a
n−
1
α
n
a
n
and
β
1
a
1
β
2
a
2
...β
n−
1
a
n−
1
β
n
a
n
where
α
i
,β
i
∈
L
.
A tuple (
x, x
,y,y
) of red nodes of the tree
T
is
H, L
-
compatible
if
x
and
x
are
H
-equivalent,
y
and
y
are
H
-equivalent,
x
and
y
are
L
-equivalent and
x
and
y
are
L
-equivalent, i.e., there exist (
α
1
, ..., α
n
)
,
(
β
1
, ..., β
n
)
H
∗
and
a
i
∈
∈
H
n
,and
L
n
such that the paths from the root to
x
,
x
,
y
,
y
are
labeled respectively by
α
1
a
1
...α
n
a
n
,
α
1
b
1
...α
n
b
n
,
β
1
a
1
...β
n
a
n
and
β
1
b
1
...β
n
b
n
.
Let
p
1
, ..., p
n
,
q
1
, ..., q
n
be the probabilities of edges labeled by
a
1
, ..., a
n
on
the path from the root to
x
(resp.
y
). Let
p
1
, ..., p
n
,
q
1
, ..., q
n
be the probabilities
of edges labeled by
b
1
, ..., b
n
on the path from the root to
x
(resp.
y
).
A
H, L
-compatible tuple (
x, x
,y,y
)is
perfect
if for every
i
=1
, ..., n
we have
p
i
/q
i
=
p
i
/q
i
.
The systems we consider are supposed to satisfy:
(
a
1
, ..., a
n
)
,
(
b
1
, ..., b
n
)
∈
(1)
Tr
is a closed subset of
E
(2) For each measurable subset
X
of
Tr
, the closure
X
is measurable and
Pr
S
(
X
)=
Pr
S
(
X
).
We start by characterizing
sequential
information flow, where the identity
of low-level events is abstracted out, and only their position in the sequence of
events is preserved.
H
ω
Theorem 1.
A probabilistic system S such that Tr
⊂
is without sequential
information flow iff
(1)
L
n
(
Tr
)
.
(2) Every H, L-compatible tuple of the tree T is perfect.
(3) For every pair of H-equivalent nodes x, x
of T , the probabilistic trees T
x
and
T
x
are isomorphic.
(4) For every n>
0(
L
n
(
Tr
)
∀
n>
0
Tr
n
=
H
n
(
Tr
)
⊗
(
H
∗
L
)
n−
1
H
ω
)=0)
.
=
∅→
Pr
S
(
Tr
∩
The intuition behind this characterization is the following: we don't want the
low-level traces to give any information on the interleavings with the high level.
Then, if a sequential high-level trace is possible, this trace can occur whatever
the trace on the low level is. Point (4) states that observing that
k
low-level
actions have occurred doesn't give any additional information, since all traces
of
Tr
have the same number of low-level events. Points (2) and (3) state that
probabilities of certain subtrees have to be equal or in equal ratios.
We give here only a sketch of the proof.
If the system has no information flow, then we prove (1), (4) and, by con-
tradiction, the existence of the same edges in
T
x
and
T
x
in (2). For the latter,
we exhibit properties for which, if one edge is not in
T
then for some
u, v
,
