Complexity of propositional LTL with past operators and freeze quantifier? In "A Really Temporal Logic", by R.Alur and A.Henziger, 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 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?
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.