Satisfiability checking of multi-variable TPTL with unilateral intervals is PSPACE-complete

DOI10.4230/LIPICS.CONCUR.2023.23MaRDI QIDQ6967324zbMATH OpenFDO

Authors Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh K. Pandya

Publication date 26 June 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2023.23

zbMATH Keywords

ATAdecidabilityexpressivenessnon-punctualitysatisfiabilityTPTL

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• A really temporal logic
• A theory of timed automata
• Alternating timed automata
• An automata-theoretic approach to linear temporal logic
• An Expressive Temporal Logic for Real Time
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities
• Expressiveness of Metric Modalities for Continuous Time
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers
• scientific article; zbMATH DE number 1256652 (Why is no real title available?)
• scientific article; zbMATH DE number 1304997 (Why is no real title available?)
• scientific article; zbMATH DE number 1759492 (Why is no real title available?)
• Implementation and Application of Automata
• Logics meet 1-clock alternating timed automata
• Mathematical Foundations of Computer Science 2003
• Memory event clocks
• On expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing
• On Process-Algebraic Extensions of Metric Temporal Logic
• On Unary Fragments of MTL and TPTL over Timed Words
• Real-time logics: Complexity and expressiveness
• Revisiting timed logics with automata modalities
• The benefits of relaxing punctuality
• The benefits of relaxing punctuality
• The compound interest in relaxing punctuality
• The unary fragments of metric interval temporal logic: bounded versus lower bound constraints
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(2)

• Metric quantifiers and counting in timed logics and automata
• Expressive equivalence between decidable freeze and metric timed temporal logics.

This page was built for publication: Satisfiability checking of multi-variable TPTL with unilateral intervals is PSPACE-complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6967324)