2026-07-23T17:30:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19017 2024-03-06T11:03:17Z ddc:004 open_access

Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete Krishna, Shankara Narayanan Madnani, Khushraj Nanik Majumdar, Rupak Pandya, Paritosh TPTL Satisfiability Non-Punctuality Decidability Expressiveness ATA 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,∞}. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Shankara Narayanan Krishna and Khushraj Nanik Madnani and Rupak Majumdar and Paritosh Pandya 2023 Is Part Of LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2023.23 urn:nbn:de:0030-drops-190171 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.23 eng https://creativecommons.org/licenses/by/4.0/legalcode