Deciding safety and liveness in TPTL

• Deciding if a TPTL formula describes a safety property is EXPSPACE-complete.
• Deciding if a TPTL formula describes a liveness property is in 2-EXPSPACE.
• We provide algorithms for these decision problems based on those for deciding safety and liveness in LTL.

We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented by Sistla [1] to decide the corresponding problems for LTL.