# Equivalent formula for LTL with and without past operators

I have recently been researching LTL with and without past operators. From my understanding, both LTL and PLTL (LTL with Past) are equally expressive, however, PLTL is exponentially more succinct.

I have been searching for a list abbreviations between LTL and PLTL formulae but have found nothing, and I cant seem to figure them out myself.

If LTL allows the formulae

• $$\bigcirc\phi$$ for $$\phi$$ is true at the next moment in time,
• $$\Diamond\phi$$ for $$\phi$$ is true some time in the future,
• $$\Box\phi$$ for $$\phi$$ is true always in the future, and
• $$\phi\mathcal{U}\psi$$ for $$\phi$$ is true until $$\psi$$ is true,

and PLTL allows the additional formulae using the past versions of the temporal operators:

1. $$\bigcirc^-\phi$$ for $$\phi$$ was true at the previous moment in time,
2. $$\Diamond^-\phi$$ for $$\phi$$ was true some time in the past,
3. $$\Box^-\phi$$ for $$\phi$$ was true always in the past,
4. $$\phi\mathcal{S}\psi$$ for $$\phi$$ has been true since $$\psi$$ was true in the past,

then how are 1-4 expressed using only LTL?

The "equally expressive" statement means that if a formula of PLTL is a statement about the future, i.e. if it's evaluated at the first instant $$0$$ of the time domain $$\mathbb N$$, then there exists an equivalent LTL formula. This means that nesting future and past operators is not more expressive than nesting just future operators, as long as the global meaning of the whole formula is solely about the future.

Here are some examples of this equivalence:

• $$\lozenge\square\lozenge^-\varphi\equiv\lozenge\varphi$$

• $$\lozenge(\alpha\wedge (\varphi \mathcal S \psi)) \equiv \lozenge (\psi \wedge (\alpha\vee \bigcirc (\varphi \mathcal U (\varphi\wedge \alpha)))$$

• So $\Diamond^-$ cannot be evaluated at 0, so there is no equivalent LTL formula? – Tyler Durden Aug 5 '19 at 16:02
• The equivalent formula is $\bot$ if you evaluate at t=0. – gigabytes Aug 5 '19 at 17:17
• Then what is the equivalent formula for any t >1 – Tyler Durden Aug 5 '19 at 19:51
• @Denis, what if a PLTL statement is a statement about the past? Are 1-4 in the original question expressible in LTL? – Tyler Durden Nov 18 '19 at 13:50
• @TylerDurden No since LTL can just speak about the future. – Denis Nov 18 '19 at 16:01