Model checking

Question

in the given graph <>{s0,s4} = {s5} so simillarly what will be the <>{ } will it be { } or {s3,s2}

Answer 1

<> phi holds on the states that have a successor state which satisfies phi. With <>{}, I guess, you mean <>false which would hold on the states which would have a successor state where false holds. However, no state can satisfy false, and therefore <>false does not hold on any state, and therefore the states satisfying <>false are {}. This is independent of a Kripke structure.

Comments

Thank You. And, what about universal predecessor for false?.

---

See slide 15 of the temporal logic chapter: []false holds on states with no successor states.