LTL to ω-automata Exam 2018.08.21 7a

Question

Please check my expanded solution:

({p,q,r,s}, q|p|r|s, 
[q <-> (a&!b) | Xq &
p<->b | Xp &
r<-> c & Xr &
s<->a| Xs],
GF[q->(a&!b)] & GF[p] &GF[c->r]&GF[s->a])

I guessed: FG !b = G[p<->b | Xp], GF[p]

Is this correct?
 

Answer 1

I don't think that it is correct, even if you follow the example solution that explains that the given formula is equivalent to F(a∧¬b) ∨ FG¬b ∨ (Gc) ∧ (Fa), you should get another automaton. When I decompile your solution, I see

    q <-> (a&!b) | Xq   --> F(a&!b)
    p <-> b | Xp        --> F(b)
    r <-> c & Xr        --> G(c)
    s <-> a | Xs        --> F(a)

However, instead of F(b), there should be FGb which is not the same. Why do you believe that it is the same?

Comments

I see. My interpretation of FG!b ended up the same as Fb.
Because I changed FG!b --> !GFb and then came up with the above automaton.

Would FG!b = p <-> !b & Xp be correct instead?
Or
Can I convert G!b first and then F() and take a conjunction after?

---

Yes, you need to first convert G!b and then F(..) so that two state variables are used. You cannot do that with just one.