Information Technology Reference
In-Depth Information
H
ω
which are without relativized se-
quential information flow are those which satisfy one of the following conditions:
(1) the projection of Tr on L is reduced to τ
ω
(2) the projection of Tr on L is a subset M of L and Tr
=
U
Theorem 4.
The only systems with Tr
⊂
⊗
(
M
×{
}
)
where
U
=
and and for every pair of H-equivalent
nodes x, x
of T , of depth one, the probabilistic trees T
(
x
)
and T
(
x
)
are
isomorphic.
{
(
α
1
,α
2
)
|
α
1
lα
2
∈
φ
(
Tr
)
}
Proof.
If the system
S
satisfies condition (1) it is easy to conclude like in
Theorem 3 that
S
is without relativized sequential information flow.
If the system
S
satisfies condition (2), the only finite non-empty traces
u ∈ L
+
such that the bunch
B
(
u
) is non-empty are actions the
a ∈ M
. Clearly for every
relativized sequential property
P
,
Pr
S
(
P, a
)=
Pr
S
(
P, b
)for
a, b ∈ M
.
Conversely, let
S
be a system without relativized sequential information flow.
Suppose that the projection of
Tr
on
L
is not reduced to
τ
ω
.Wehavetoprove
that
S
satisfies (2). The projection of
Tr
on
L
cannot contain a trace
w
with
more than one action and different from
τ
ω
. Indeed suppose that
w
=
abw
,
a, b
H
∗
,and
λ
L
)
ω
.
∈
L
.Then
Tr
contains a trace
αaβbλ
,where
α, β
∈
∈
(
H
∪
)
ω
.
Consider now the relativized sequential property
P
=
{
αl
}×{
βl
}
(
H
∪{
l
}
We have
Pr
S
(
P, a
)
=0and
Pr
S
(
P, ab
) = 0. Contradiction. So the projection of
Tr
on
L
is a subset
M
of
L
. Let us prove that
Tr
=
U
⊗
(
M
×{
}
). Suppose
that there exists
α
1
lα
2
∈
φ
(
Tr
)andsome
a
∈
M
such that
α
1
aα
2
∈
Tr
.Then
)
ω
:
Pr
S
(
P, a
)=0
there is information flow for the property
P
=
{
αl
}×
(
H
∪{
l
}
and there exists
b
= 0. Proving the other conditions of
(2) is straightforward, following steps of the proof of Theorem 1.
∈
M
such that
Pr
S
(
P, b
)
The absence of relativized sequential information flow is a very strong prop-
erty, and as seen from the conditions in Theorem 4, very few probabilistic event
systems have this property. This stems from the fact that, in expressing the
property
P
, a trace is split into two parts, just after the occurrence of a low-
level event. If it is possible to observe more or fewer low-level actions in a trace
than specified in the property, there is information flow.
But it is still interesting to consider low-level traces of the same length
n
,
and examine if they give some additional high-level information (besides the fact
that
n
low-level events have occurred). We are then interested in a weaker notion
of “no information flow” for a relativized sequential property, namely:
Definition 7.
AsystemS is without information flow at each fixed step for a
relativized property P if Pr
S
(
P, u
)=
Pr
S
(
P, v
)
for every u, v
L
+
∈
such that
|
u
|
=
|
v
|
and B
(
u
)
,B
(
v
)
are non-empty.
In order to characterize the systems without sequential relativized information
flow at each fixed step we need to introduce a new definition. In the probabilistic
tree
T
of the system, the
red depth
of a node is the number of red edges on the
path from the root to it.
Theorem 5.
AsystemS such that Tr
H
ω
⊂
is without sequential relativized
information flow at each fixed step iff
