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?


1 Answer 1


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

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

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.