1
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ So $\Diamond^-$ cannot be evaluated at 0, so there is no equivalent LTL formula? $\endgroup$ – Tyler Durden Aug 5 at 16:02
  • $\begingroup$ The equivalent formula is $\bot$ if you evaluate at t=0. $\endgroup$ – gigabytes Aug 5 at 17:17
  • $\begingroup$ Then what is the equivalent formula for any t >1 $\endgroup$ – Tyler Durden Aug 5 at 19:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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