NI generalization

In this section we present the Non Deducibility on Compositions (NDC, for short) property, proposed in [FG95] as a generalization of NI in a process algebraic setting. It is simply based on the idea of checking the system against all high level potential interactions. A system E is NDC if for every high level process $\Pi$ a low level user cannot distinguish E from $(E\vert\Pi)\setminus Act_H$. In other words, a system E is NDC if what a low level user sees of the system is not modified by composing any high level process $\Pi$ to E .

Definition 2.2

E is NDC if and only if $\forall \Pi \in {\cal E}_{H}$, $E / Act_H \approx_T (E \mid \Pi) \setminus Act_H$. $\rule{2mm}{2mm}$

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

 $E \in \mbox{{\it SNNI}\/} \Longleftrightarrow E \setminus Act_H \approx_T E / Act_H$. $\rule{2mm}{2mm}$

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 $\gamma$ of the system containing some high level actions. Then, we look if there exists another trace $\gamma'$ 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 $\gamma$ and $\gamma'$. As both $\gamma$ and $\gamma'$ are legal traces, we can conclude that the possible execution of the high level actions in $\gamma$ has no effect on the low level view of the system. As a matter of fact, in $E / Act_H$ all the high level actions are hidden, hence giving the low level view of the system; $E \setminus Act_H$ 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 $\rule{2mm}{2mm}$

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.