<p>The answer was buried in a small section of the same paper that I was citing. Adding past operators to TPTL, in contrast of what happens with LTL, causes a huge increase in complexity as the satisfiability problem becomes <em>non-elementary</em>.</p>

<p>The fact is proven in the paper by showing how a mixture of future and past operators, combined with the freeze quantifier, can emulate an arbitrary first-order existential quantifier. </p>

CC BY-SA 3.0
2018-02-15T04:35:59.063Z
2018-02-15T10:13:20.457Z
2018-02-15T10:13:20.457Z
Nicola Gigante
<p>In <a href="http://dl.acm.org/citation.cfm?id=174651" rel="nofollow noreferrer">"A Really Temporal Logic", by R.Alur and A.Henziger</a>, they introduce an extension of Linear Temporal Logic with a <em>freeze quantifier</em> <span class="math-container">$x.\phi$</span>, which allows to "give a name" to the current time point to later compare it with others. An example formula from the paper is</p>

<p><span class="math-container">$$
\Box x.(p \to \Diamond y.(q \land y \le x + 10))
$$</span></p>

<p>which means that whenever <span class="math-container">$p$</span> holds, <span class="math-container">$q$</span> must eventually hold within 10 time points. This logic has been proved to be EXPSPACE-complete in the above paper.</p>

<p>Since the paper is very old, I'm wondering which developments have been done on this logic. 
Specifically, I'm asking if it has been proved whether this logic augmented with LTL <em>past</em> operators is still EXPSPACE-complete, as is the case for classic LTL+past which remains PSPACE-complete as the future-only version.</p>

<p>I've found something by searching for "freeze quantifier" but recent works such as <a href="http://dl.acm.org/citation.cfm?id=1507246" rel="nofollow noreferrer">this paper</a> talk about further extensions with registers that I'm not interested about (or maybe I am but I'm misunderstanding).</p>

<p>So is this logic augmented with past operators still EXPSPACE-complete?</p>

CC BY-SA 3.0
2016-06-07T18:25:39.573Z
The EXPSPACE bound is attained by using a tableau, which is very similar to an automaton. Traditionally, in order to tackle past operators, one translates to a 2-way automaton, and from there to a standard automaton. Thus, perhaps you can try constructing a 2-way automaton based on the construction in the paper.
Shaull
CC BY-SA 3.0
2016-06-08T09:54:22.270Z
So it is at least plausible? I'm currently trying to understand if I can inject the techniques used by their tableau into the one used by Lichtenstein and Pnueli in "Propositional Temporal Logics: Decidability and Completeness".
Nicola Gigante
CC BY-SA 3.0
2016-06-08T09:58:21.840Z
Well, it might be possible. It seems like a natural extension to study, and it seems not to have been studied yet.
If you just want a yes/no answer, your best bet is to contact Tom Henzinger directly, he might have an easy answer, or he might tell you that it needs to be studied carefully.
Shaull
CC BY-SA 3.0
2016-06-08T10:19:35.203Z
I'm always a bit shy in emailing authors for stuff like these, especially big names... :)
Nicola Gigante
CC BY-SA 3.0
2016-06-08T11:36:33.247Z
A polite email regarding someone's research is always welcome, in my experience.
Shaull
<reference-request><temporal-logic><linear-temporal-logic><complexity>
Complexity of propositional LTL with past operators and freeze quantifier?
Nicola Gigante
# Complexity of propositional LTL with past operators and freeze quantifier?

(Asked by: username_0 on 2016-06-07)

In ["A Really Temporal Logic", by R.Alur and A.Henziger](http://dl.acm.org/citation.cfm?id=174651), they introduce an extension of Linear Temporal Logic with a *freeze quantifier* $x.\phi$, which allows to "give a name" to the current time point to later compare it with others. An example formula from the paper is

$$
\Box x.(p \to \Diamond y.(q \land y \le x + 10))
$$

which means that whenever $p$ holds, $q$ must eventually hold within 10 time points. This logic has been proved to be EXPSPACE-complete in the above paper.

Since the paper is very old, I'm wondering which developments have been done on this logic.
Specifically, I'm asking if it has been proved whether this logic augmented with LTL *past* operators is still EXPSPACE-complete, as is the case for classic LTL+past which remains PSPACE-complete as the future-only version.

I've found something by searching for "freeze quantifier" but recent works such as [this paper](http://dl.acm.org/citation.cfm?id=1507246) talk about further extensions with registers that I'm not interested about (or maybe I am but I'm misunderstanding).

So is this logic augmented with past operators still EXPSPACE-complete?

**Tags:** reference-request, temporal-logic, linear-temporal-logic, complexity

> **Comments:**
> **username_1**: The EXPSPACE bound is attained by using a tableau, which is very similar to an automaton. Traditionally, in order to tackle past operators, one translates to a 2-way automaton, and from there to a standard automaton. Thus, perhaps you can try constructing a 2-way automaton based on the construction in the paper.  
> **username_0**: So it is at least plausible? I'm currently trying to understand if I can inject the techniques used by their tableau into the one used by Lichtenstein and Pnueli in "Propositional Temporal Logics: Decidability and Completeness".  
> **username_1**: Well, it might be possible. It seems like a natural extension to study, and it seems not to have been studied yet. If you just want a yes/no answer, your best bet is to contact Tom Henzinger directly, he might have an easy answer, or he might tell you that it needs to be studied carefully.  
> **username_0**: I'm always a bit shy in emailing authors for stuff like these, especially big names... :)  
> **username_1**: A polite email regarding someone's research is always welcome, in my experience.  

---

## 1 answers

### Answer by username_0 on 2018-02-15. Score: 3 | Accepted answer

The answer was buried in a small section of the same paper that I was citing. Adding past operators to TPTL, in contrast of what happens with LTL, causes a huge increase in complexity as the satisfiability problem becomes *non-elementary*.

The fact is proven in the paper by showing how a mixture of future and past operators, combined with the freeze quantifier, can emulate an arbitrary first-order existential quantifier.


---

