<p>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 <span class="math-container">$0$</span> of the time domain <span class="math-container">$\mathbb N$</span>, 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.</p>

<p>Here are some examples of this equivalence: </p>

<ul>
<li><p><span class="math-container">$\lozenge\square\lozenge^-\varphi\equiv\lozenge\varphi$</span> </p></li>
<li><p><span class="math-container">$\lozenge(\alpha\wedge (\varphi \mathcal S \psi)) \equiv \lozenge (\psi \wedge (\alpha\vee \bigcirc (\varphi \mathcal U (\varphi\wedge \alpha)))$</span></p></li>
</ul>

CC BY-SA 4.0
2019-08-05T16:02:39.973Z
So $\Diamond^-$ cannot be evaluated at 0, so there is no equivalent LTL formula?
Tyler Durden
CC BY-SA 4.0
2019-08-05T17:17:24.740Z
The equivalent formula is $\bot$ if you evaluate at t=0.
Nicola Gigante
CC BY-SA 4.0
2019-08-05T19:51:37.020Z
Then what is the equivalent formula for any t >1
Tyler Durden
CC BY-SA 4.0
2019-11-18T13:50:25.550Z
@Denis, what if a PLTL statement is a statement about the past? Are 1-4 in the original question expressible in LTL?
Tyler Durden
CC BY-SA 4.0
2019-11-18T16:01:53.703Z
@TylerDurden No since LTL can just speak about the future.
Denis
CC BY-SA 4.0
2019-08-05T12:25:00.373Z
2019-08-05T12:25:00.373Z
Denis
<p>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.</p>

<p>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. </p>

<p>If LTL allows the formulae </p>

<ul>
<li><span class="math-container">$\bigcirc\phi$</span> for  <span class="math-container">$\phi$</span> is true at the next moment in time,</li>
<li><span class="math-container">$\Diamond\phi$</span> for  <span class="math-container">$\phi$</span> is true some time in the future,</li>
<li><span class="math-container">$\Box\phi$</span> for  <span class="math-container">$\phi$</span> is true always in the future, and</li>
<li><span class="math-container">$\phi\mathcal{U}\psi$</span> for  <span class="math-container">$\phi$</span> is true until <span class="math-container">$\psi$</span> is true,</li>
</ul>

<p>and PLTL allows the additional formulae using the past versions of the temporal operators:</p>

<ol>
<li><span class="math-container">$\bigcirc^-\phi$</span> for  <span class="math-container">$\phi$</span> was true at the previous moment in time,</li>
<li><span class="math-container">$\Diamond^-\phi$</span> for  <span class="math-container">$\phi$</span> was true some time in the past,</li>
<li><span class="math-container">$\Box^-\phi$</span> for  <span class="math-container">$\phi$</span> was true always in the past,</li>
<li><span class="math-container">$\phi\mathcal{S}\psi$</span> for  <span class="math-container">$\phi$</span> has been true since <span class="math-container">$\psi$</span> was true in the past,</li>
</ol>

<p>then how are 1-4 expressed using only LTL?</p>

<temporal-logic><linear-temporal-logic>
Equivalent formula for LTL with and without past operators
Tyler Durden
# Equivalent formula for LTL with and without past operators

(Asked by: username_0 on 2019-08-05)

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?

**Tags:** temporal-logic, linear-temporal-logic


---

## 1 answers

### Answer by username_1 on 2019-08-05. Score: 2

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

> **Comments:**
> **username_0**: So $\Diamond^-$ cannot be evaluated at 0, so there is no equivalent LTL formula?  
> **username_2**: The equivalent formula is $\bot$ if you evaluate at t=0.  
> **username_0**: Then what is the equivalent formula for any t >1  
> **username_0**: @username_1, what if a PLTL statement is a statement about the past? Are 1-4 in the original question expressible in LTL?  
> **username_1**: @TylerDurden No since LTL can just speak about the future.  

---

