Exam Problem : 29.08.2017 : Q 8 e : 2017.08.29.vrs.solutions.pdf (uni-kl.de)

Problem :

My Solution :

I thought it like below to satisfy S1 and not S2:

X !a holds in {s0, s1, s2}

!a holds in {s0, s2}

!a & X !a holds in {s0, s2}

AF (!a & X !a) holds in {s0, s2}

Hence it satisfies S1.

X !a holds in {s0, s1, s2}

AX !a holds in {s1, s2}

!a & AX !a holds in {s2}

AF (!a & AX !a) holds in {s1, s2} => (There is path in s0 in which it can loop forever and never reach s2)

No initial set, hence not satisfied.

Q1. Could you please let me know if my Kripke Structure is correct ?

Q2. Could you please let me know if my way of proofing is correct ?

Thanks in advance