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}$.

翻译：本文研究定时命题时序逻辑（TPTL）的${0,\infty}$片段的可判定性。我们证明TPT L$^{0,\infty}$的可满足性检测是PSPACE完全的。此外，即使其单变量片段（1-TPTL$^{0,\infty}$）在表达能力上也严格强于度量区间时序逻辑（MITL），而MITL的可满足性检测是EXPSPACE完全的。因此，我们得到了一个表达能力更强且可满足性检测计算复杂度更低的逻辑。据我们所知，TPTL$^{0,\infty}$是首个在不对定时字施加任何有界性/限制（如有界变异性、有界时间等）的情况下，可满足性检测可判定的TPTL多变量片段。PSPACE成员资格通过归约为一种新型"非精确"多时钟交替定时自动机子类——单侧极弱交替定时自动机（VWATA$^{0,\infty}$）的空性检测问题得到证明，我们已证明该自动机类属于PSPACE。我们通过构造一个等价模拟的非确定性定时自动机来证明这一点，该自动机的时钟数量与给定VWATA$^{0,\infty}$的规模呈多项式关系。