Openness And Partial Adjacency In One Variable TPTL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910680261591040 |
|---|---|
| author | Krishna, Shankara Narayanan Madnani, Khushraj Nag, Agnipratim Pandya, Paritosh |
| author_facet | Krishna, Shankara Narayanan Madnani, Khushraj Nag, Agnipratim Pandya, Paritosh |
| contents | Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) extend Linear Temporal Logic (LTL) for real-time constraints, with MTL using time-bounded modalities and TPTL employing freeze quantifiers. Satisfiability for both is generally undecidable; however, MTL becomes decidable under certain non-punctual and partially-punctual restrictions. Punctuality can be restored trivially under similar non-punctual restrictions on TPTL even for one variable fragment. Our first contribution is to study more restricted notion of openness for 1-TPTL, under which punctuality can not be recovered. We show that even under such restrictions, the satisfiability checking does not get computationally easier. This implies that 1-TPTL (and hence TPTL) does not enjoy benefits of relaxing punctuality unlike MTL. As our second contribution we introduce a refined, partially adjacent restriction in 1-TPTL (PA-1-TPTL), and prove decidability for its satisfiability checking. We show that this logic is strictly more expressive than partially punctual Metric Temporal Logic, making this as one of the most expressive known boolean-closed decidable timed logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_00117 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Openness And Partial Adjacency In One Variable TPTL Krishna, Shankara Narayanan Madnani, Khushraj Nag, Agnipratim Pandya, Paritosh Logic in Computer Science Formal Languages and Automata Theory 03B44 F.4.1; F.4.3 Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) extend Linear Temporal Logic (LTL) for real-time constraints, with MTL using time-bounded modalities and TPTL employing freeze quantifiers. Satisfiability for both is generally undecidable; however, MTL becomes decidable under certain non-punctual and partially-punctual restrictions. Punctuality can be restored trivially under similar non-punctual restrictions on TPTL even for one variable fragment. Our first contribution is to study more restricted notion of openness for 1-TPTL, under which punctuality can not be recovered. We show that even under such restrictions, the satisfiability checking does not get computationally easier. This implies that 1-TPTL (and hence TPTL) does not enjoy benefits of relaxing punctuality unlike MTL. As our second contribution we introduce a refined, partially adjacent restriction in 1-TPTL (PA-1-TPTL), and prove decidability for its satisfiability checking. We show that this logic is strictly more expressive than partially punctual Metric Temporal Logic, making this as one of the most expressive known boolean-closed decidable timed logic. |
| title | Openness And Partial Adjacency In One Variable TPTL |
| topic | Logic in Computer Science Formal Languages and Automata Theory 03B44 F.4.1; F.4.3 |
| url | https://arxiv.org/abs/2411.00117 |