Seite 1 von 1

### Module 8 - GNI

Verfasst: 22. Jun 2012 14:30
In the lecture I think Prof. Mantel provided a formal definition of GNI like this:

$$\forall \tau \in Tr. \forall \alpha',\beta' \in E^*. (\exists \alpha, \beta \in E^*: \tau = \alpha.\beta \land \alpha' = \alpha \land \beta'_{|E \setminus (H \cap I)} = \beta_{|E \setminus (H \cap I)}) \Rightarrow (\exists \alpha'',\beta'' \in E^*: \alpha''.\beta'' \in Tr \land \alpha' = \alpha'' \land \beta'_{|(H \cap I) \cup L} = \beta''_{|(H \cap I) \cup L})$$

However I don't think that this formula captures the intuition of "after the first changed input" correctly.

If we take the example of $$SES_A$$ on slide 59, it is stated that while $$\langle 1, 2, 1, 3, stop, ev_A \rangle \in Tr$$ is a valid one, the trace $$\langle 1, 2, 3, 1, stop, ev_A \rangle \in Tr$$ is not a permissible correction of the perturbation $$\langle 1, 2, 1, stop, ev_A \rangle$$ of $$\langle 1, 2, stop, ev_A \rangle$$, because it adds the high output event 3 BEFORE the first change high input event 1.

But in the formula above, we could set $$\alpha' = \alpha = \alpha'' = \langle 1, 2 \rangle$$ and $$\beta' = \langle 1, stop, ev_A \rangle$$, $$\beta = \langle stop, ev_A \rangle$$ and $$\beta'' = \langle 3, 1, stop, ev_A \rangle$$, such that the formula is fulfilled.

So is the formula wrong or am I missunderstanding something?