# CTL* to LTL conversion I am confused with the 2nd step here.

1st step - Conversion because of Negation (!E(a)=A!(a))

2nd step = ?? (AGA = G) ??

3rd step - Conversion to until operator. (Ga = ![1 SU !a])

The first step is driving in the negation, as you wrote. The second step does not tell you that AGA=G holds, instead, consider A!a which holds in a state where all outgoing paths must satisfy !a. Hence, that is nothing else than (A false) | !a, so that we get AG(A!a) = AG((A false) | !a). A false only holds in states with no infinite paths which are ignored by AG, so that the latter is equivalent to AG!a.

Then, we have A(AG!a & A![Fb SU !c]) where we can pull out the A quantifier and get AA(G!a & ![Fb SU !c]) which is the same as A(G!a & ![Fb SU !c]).

It is a common mistake to consider some of these replacements are equivalences that should be generally valid. However, they appear in a context and are only valid in that context. For instance, A!a is not equivalent to !a only, but in the context above, it is so, since the other disjunction A false is wiped out.
by (144k points)
selected by