Complexity of propositional LTL with past operators and freeze quantifier?
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.