Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

510 users

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)

https://es.cs.uni-kl.de/teaching/vrs/exams/2018.08.21.vrs/2018.08.21.vrs.solutions.pdf

Update:

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