Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

We investigate the decidability of the 0,∞ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL0,∞ is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL0,∞) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL0,∞ is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual" subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA0,∞) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA0,∞.