Hello everyone,
If we are supposed to determine a simulation relation, like for example in exam 2017.08 , before computing the fixpoint iterations to check SIM2, it can be seen that SIM3 cannot be satisfied, since their is no relation between the initials. Would it be sufficient enough to directly state that SIM3 cannot be fullfilled, without performin the whole algorithm?
Thanks in Advance.