本文研究了Timed Propositional Temporal Logic (TPTL)的{0,∞}分片的可决定性，并证明了TPTL^{0,∞}的可满足性检查为PSPACE-complete。此外，1-TPTL^{0,∞}比Metric Interval Temporal Logic (MITL)更具表达能力，后者的可满足性检查是EXPSPACE complete。因此，TPTL^{0,∞}是第一个多变量TPTL分片，其可满足性检查在没有对时态词施加任何限制的情况下是可决定的。通过将其规约到Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞})的空泛性检查问题，我们证明了PSPACE的成员关系。