CTL LTL Feb 2022 7b

Question

I hope you are able to check my solution attached. 

I tried to satisfy S2. Considering the s2 satisfies a and s0s1 path satisfies FGb.

{a}<--{Init.} -->inf.{b}

Is my solution right?

 I tried to solve similar to Sept 2022 7d question.

Answer 1

Do you mean this structure?

The path s0->s1^omega satisfies [a SU FGb], but it does not satisfy  [a SU Gb], which is no surprise since that path is the one given in the example solution. Why did you add the other state s2?

Comments

I just wanted to understand conceptually that with state s2 still, S2 condition is satisfied?

---

Yes, it is. However, since the formulas are path formulas, you should also mention which path you consider to distinguish the two formulas, and there you would have to consider the path of the example solution.

---

Got it. Thank you so much.