5
$\begingroup$

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?

| cite | improve this question | | | | |
$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – Shaull Jun 7 '16 at 18:25
  • $\begingroup$ 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". $\endgroup$ – gigabytes Jun 8 '16 at 9:54
  • $\begingroup$ 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. $\endgroup$ – Shaull Jun 8 '16 at 9:58
  • $\begingroup$ I'm always a bit shy in emailing authors for stuff like these, especially big names... :) $\endgroup$ – gigabytes Jun 8 '16 at 10:19
  • 5
    $\begingroup$ A polite email regarding someone's research is always welcome, in my experience. $\endgroup$ – Shaull Jun 8 '16 at 11:36
3
$\begingroup$

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.

| cite | improve this answer | | | | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.