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

TL;DR

This paper proves that satisfiability checking for a specific fragment of Timed Propositional Temporal Logic (TPTL) is PSPACE-complete, and introduces a new automata class to establish decidability without bounds on timed words.

Contribution

It demonstrates PSPACE-completeness of TPTL$^{0, ext{infinity}}$ satisfiability and introduces Unilateral Very Weak Alternating Timed Automata to achieve decidability.

Findings

TPTL$^{0, ext{infinity}}$ is PSPACE-complete.

1-variable TPTL$^{0, ext{infinity}}$ exceeds MITL in expressiveness.

Decidability achieved without bounds on timed words.

Abstract

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