Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals
  Is PSPACE-Complete
Shankara Narayanan Krishna Khushraj Nanik Madnani Rupak Majumdar Paritosh K. Pandya
We investigate the decidability of the ${0,\infty}$ fragment of Timed
Propositional Temporal Logic (TPTL). We show that the satisfiability checking
of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable fragment
(1-TPTL$^{0,\infty}$) 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, TPTL$^{0,\infty}$ 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 (VWATA$^{0,\infty}$) 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 VWATA$^{0,\infty}$.