DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.23

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

Authors: Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

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,∞}.

Cite as

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya. Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krishna_et_al:LIPIcs.CONCUR.2023.23,
  author =	{Krishna, Shankara Narayanan and Madnani, Khushraj Nanik and Majumdar, Rupak and Pandya, Paritosh},
  title =	{{Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.23},
  URN =		{urn:nbn:de:0030-drops-190171},
  doi =		{10.4230/LIPIcs.CONCUR.2023.23},
  annote =	{Keywords: TPTL, Satisfiability, Non-Punctuality, Decidability, Expressiveness, ATA}
}

Search Results

Documents authored by Madnani, Khushraj Nanik

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

Abstract

Cite as

Thanks for your feedback!

Could not send message