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

2023/09/01 by Krishna, Shankara Narayanan, Madnani, Khushraj Nanik, Majumdar, Rupak +1 · 1 citation
#Computation and Language (cs.CL) #F.1.1 #F.4 #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2309.00386

Abstract

We investigate the decidability of the 0,∞ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL^0,∞ is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL^0,∞) 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,∞ 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,∞) 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,∞.

Cited by

• MightyPPL: Verification of MITL with Past and Pnueli Modalities

Related

• Generalizing Non-Punctuality for Timed Temporal Logic with Freeze\n Quantifiers
• Openness And Partial Adjacency In One Variable TPTL
• Revisiting Timed Logics with Automata Modalities
• On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
• Revisiting MITL to Fix Decision Procedures