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 hold, 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?
Complexity of propositional LTL with past operators and freeze quantifier?
reference request;temporal logic;linear temporal logic;complexity