CTL* model checking

Question

why it holds only for s1 and not s2. Kindly elaborate.

Answer 1

Property S1 holds in state s0, since all paths leaving states s0 satisfy next p or q: We have p next when we go left, and q next when we go right. Property S2 does not hold in state s0 since neither do all paths leaving state s0 satisfy next p, nor do all paths leaving state s0 satisfy next q.

Comments

Thanks a lot. It resolved my confusion now.