Definition 2.2
E is NDC if and only if ,
.
This definition of NDC is difficult to use in practice, because of the universal quantification on high level processes. We need an alternative formulation of BNDC which avoids universal quantification, exploiting local information only. It is possible to prove [FG95] that NDC is equivalent to Strong Non-deterministic Non Interference (SNNI, for short) which is defined as follows:
Definition 2.3
This property is a natural generalization of NI to non-deterministic
systems. Intuitively, the high level does not interfere with the low level
if the effects of high level actions are not visible by a low level user. In
order to check this, we consider every trace of the system
containing some high level actions. Then, we look if there exists another
trace
with the same subsequence of low level actions and without
any high actions. A low level user, which can only observe low level
actions, is not able to distinguish
and
. As both
and
are legal traces, we can conclude that the possible
execution of the high level actions in
has no effect on the low
level view of the system. As a matter of fact, in
all the high
level actions are hidden, hence giving the low level view of the system;
instead removes all the traces containing high level
actions. So, if the two terms are equivalent, then for every trace with high
level actions we can find another trace without such actions but with the
same subsequence of low level actions.
We have the following result [FG95]:
Proposition 2.4
NDC = SNNI
It is interesting to observe that this characterization of NDC through the SNNI property is possible since we are using an equivalence notion which is not able to detect deadlocks. In [FG95,FG] it is shown that under finer equivalence notions (testing, bisimulation) this result does not hold and a good (i.e., easy to check) characterization of NDC is still to be found.