Consider the LTS: M ≡ h{s0, s1, s2, s3}, {s0}, {(s0, s1),(s0, s3),(s1, s1),(s1, s2),(s2, s0),(s2, s3),(s3, s0)}, Li
where L assigns {p1, p2} to s0, {p3} to s1, {p1, p4} to s2, and {p2, p3} to s3. For each of the following
CTL wffs φ, determine whether or not M φ. If the answer is yes, briefly justify your answer;
otherwise, provide a counterexample trace/path.
(a) AFp2
(b) AG(EF(p1 ∨ p3))
(c) EX(EXp3)
(d) AG(AFp2)