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

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar +1

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-c…