Simulation Question Aug 23

Question

In the part b of simulation question the initial state is not present in the final states set, still answer is given as property holds, also all the initial states set should be present to make it hold, moreover q4 isnt the initial state which is mentioned in the description given

Answer 1

This is in fact a printing mistake. In the second Kripke structure q4 was supposed to be the only initial state which would lead to K2 <= K1 holding.