# August 2018; Problem 7b Prove validity of FFGa <-> FGa

Hi, in this Problem we need to prove validity of FFG<->FGa using the steps of building a w-Automata for the negation and then saying there is no infinite path fulfilling the acceptance condition.

My approach would be to make the dnf of !a<->b, then build w-automata for each minterm and make a union of these minterm automata. We had no rule of making the xor  of 2 automata.  This is sadly very slow,  is there a better Method ?

+1 vote

Well, you neither need an equivalence nor an xor of automata, since the LTL translation procedure will abbreviate the temporal operators by state formulas q0,q1,q2, so that we obtain at the end the formula q1<->q2 which will define the initial states of the automaton.

But if you want to go a more complicated way, you can, of course replace the equivalence by !,&,| and would, for instance, obtain (FFGa & FGa) | (!FFGa & !FGa) which is equivalent to (FFGa & FGa) | (GGF!a & GF!a). From here you can produce the omega automata and you now just need conjunction and disjunction.

Note that equivalence and xor can be reduced to that, so that we finally don't have to define equivalence and xor on the automata. Since these operations have negative occurrences, they are not that easy to define on the automata, unless the latter are deterministic ones.
by (166k points)
selected by
Just to be clear, why do 3 states suffice? Is it Ga, q0 , FGa, q1,FFGa ,q2?
Yes, that is the meaning of the three state variables.