Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Openness And Partial Adjacency In One Variable TPTL

Shankara Narayanan Krishna, Khushraj Madnani, Agnipratim Nag, Paritosh Pandya

TL;DR

A refined, partially adjacent restriction in 1-TPTL (PA-1-TPTL), and it is shown 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.

Abstract

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.

Openness And Partial Adjacency In One Variable TPTL

TL;DR

A refined, partially adjacent restriction in 1-TPTL (PA-1-TPTL), and it is shown 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.

Abstract

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.

Paper Structure

This paper contains 32 sections, 16 theorems, 13 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Linear Temporal Logic
  4. Metric Temporal Logic
  5. Syntax
  6. Semantics
  7. Natural Subclasses of $\mathsf{MTL}$
  8. Metric Interval Temporal Logic ($\mathsf{MITL}$)
  9. The Until Only Fragment of $\mathsf{MTL}$ ($\mathsf{MTL}[\:\mathsf{U}_I]$)
  10. Partially Punctual Metric Temporal Logic, PMTL
  11. Timed Propositional Temporal Logic
  12. Satisfiability Checking for Open TPTL
  13. Open $\mathsf{TPTL}$ with 1 Variable ($\hbox{$\mathsf{OpTPTL}^1$}$)
  14. Counter Machines
  15. Incremental Error Counter Machine ($\mathsf{IECM}$)
  16. ...and 17 more sections

Key Result

Theorem 2.1

Satisfiability checking for $\mathsf{MITL}$ is decidable over both finite and infinite timed words with EXPSPACE-complete complexity.

Figures (2)

  • Figure 4: Figure showing semantics of $\mathsf{FRat}^k_{I_1,\ldots,I_k}(\mathsf{A}_1, \mathsf{A}_2, \ldots, \mathsf{A}_{k},\mathsf{A}_{k+1})(S)$.
  • Figure 5: Figure showing the reduction of $\mathcal{F}^2_{[l_1,u_1],[l_2,u_2]}(\mathsf{A}_1, \mathsf{A}_2, \mathsf{A}_3)(S)$ to formulae using only $\mathsf{Rat}_I$ modalities.

Theorems & Definitions (20)

  • Theorem 2.1: AFH96
  • Theorem 2.2: Ouaknine05 OuaknineW06
  • Theorem 3.1
  • Theorem 3.2
  • Theorem 3.3
  • proof
  • Theorem 4.1
  • Theorem 4.2
  • Theorem 4.3
  • Theorem 4.4
  • ...and 10 more