Seite 1 von 1

Module 8 - GNI

Verfasst: 22. Jun 2012 14:30
von franzose
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?

Thanks for your help!

Re: Module 8 - GNI

Verfasst: 27. Jun 2012 16:34
von Sarah Ereth
Yes, I aggree with you that your choice of a valuation does not provide a counterexample to the satisfaction of the formula.

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 :-)

Re: Module 8 - GNI

Verfasst: 27. Jun 2012 18:07
von franzose
Thank you very much for your reply :)