# Getting rid of "FG" in a LTL equation

i am currently struggling with a Linear temporal logic equation: $$\phi=FG( \lnot a\lor X \lnot a )$$ For my understanding, it means that starting at a certain point in the future, proposition a can never be reached again due to the definiton of "finally globally".

Now we have to transform it into an aquivalent equation that only contains the "Until" (U) "Next" (X), $$\lnot$$ and $$\land$$ operator.

My first approach was "everything allowed until never a again" but for that i would need "F" or "g" again, or am i getting something wrong?

Thinking about this problem for quite some days now, my prof said it was pretty easy but i just cannot figure it out, i hope some of you guys can help me :D Thanks in advance! Enjoy your day :)

Not a full solution, but a guide: First, note that the meaning of $$G$$ is "always" (or "globally"), not "never". Thus, $$FG$$ means "from a certain point and on" (or in LTL phrasing: eventually always). The intuitive meaning of the formula $$FG(\neg a\vee X\neg a)$$ is that from somepoint and on, either you see $$\neg a$$ now, or in the next step.
However, all this is unnecessary in order to convert the formula to the temporal operator $$U$$ -- the operators $$F$$ and $$G$$ are built from $$U$$, and the translation is completely mechanical, using the following definitions:
• $$F\phi=\text{true}U \phi$$
• $$G\phi=\neg F\neg \phi$$
• Thank you, that helped. So at first, i apply the second rule to get $F \lnot F \lnot ( \lnot a \lor X \lnot a )$ . After that the first one + DeMorgan to then have $true U ( \lnot true U ( a \land X a ) )$ ? I Know the concept of tautology and contradiction but the combination of $\lnot$ and Until is confusing me. Thank you in advance for your patience Dec 6, 2021 at 15:25