Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers

Conference paper (2021)

Authors

Shankara Narayanan Krishna Indian Institute of Technology Bombay
K.N. Madnani Team Manuel Mazo Jr - Mechanical, Maritime and Materials Engineering
M. Mazo Team Manuel Mazo Jr - Mechanical, Maritime and Materials Engineering
Paritosh K. Pandya Indian Institute of Technology Bombay
Research Group
Team Manuel Mazo Jr (Mechanical, Maritime and Materials Engineering) (TU Delft)
Copyright: © 2021 Shankara Narayanan Krishna, K.N. Madnani, M. Mazo, Paritosh K. Pandya
DOI
help_outline
https://doi.org/10.1007/978-3-030-90870-6_10
More Info
expand_more

Published Date

2021

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Mechanical, Maritime and Materials Engineering

Department

Delft Center for Systems and Control

Research Group

Team Manuel Mazo Jr

Abstract

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.