Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.
Prove the LTL formula (FFGa) ↔ (FGa) to be valid by applying these steps: Translate the negation of the formula to a symbolic ω-automaton.
In the solution's acceptance condition there are three GF's conjuncted. First one is GF[a -> q0], this one is clearly Ga's omega translation. The next GF[q1 -> q0] and GF[q2 -> q1] are Fa's translation.
My question is why did we only considered the first part FFGa although the problem asks to translate the negation of whole formula? (after negation of <-> it becomes xor)
Professor answered on https://q2a.cs.uni-kl.de/1835/august-2018-problem-7b-prove-validity-of-ffga-fga
When we make the abbreviations, we first get