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 :)


1 Answer 1


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$

Simply apply these rules, and you'll have your formula.

  • $\begingroup$ 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 $\endgroup$ Dec 6, 2021 at 15:25
  • $\begingroup$ Yes. Looks good. $\endgroup$
    – Shaull
    Dec 6, 2021 at 15:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.