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?

Furthermore, I also agree with you that the formula is not as restrictive as the informal description. You can find an alternative formal definition in the solution to Exercise 10.5.b) and finally, i.e. in the next lecture, you will see a satisfactory formal definition of GNI using MAKS Thank you very much for your reply 