|
| | | | |
| | | |
| Stat |
Members: 3665
Articles: 2'599'751
Articles rated: 2609
17 January 2025 |
|
| | | | |
|
Article overview
| |
|
|
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete | | Shankara Narayanan Krishna
; Khushraj Nanik Madnani
; Rupak Majumdar
; Paritosh K. Pandya
; | | Date: |
1 Sep 2023 | | 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}$. | | Source: | arXiv, 2309.00386 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|
REGISTER