Complexity of metric temporal logics with counting and the Pnueli modalities
type: Item
instance of: scholarly article
title: Complexity of metric temporal logics with counting and the Pnueli modalities
zbMATH Open document ID: 1196.03029
author: Alexander Rabinovich
published in: Theoretical Computer Science
publication date: 2010-05-27T00:00:00Z
review text: This paper further develops the theory of metric temporal logics over continuous time. More specifically, the paper studies the complexity of the satisfiability problem for the logics TLC and TLP. Here, TLC is the temporal logic with Until and Since operators extended with counting modalities \(C_k(X)\) that express that ``\(X\) is true at least \(k\) times in the unit interval ahead''. TLP is the temporal logic with Until and Since operators extended with the so-called Pnueli modalities \(\mathrm{Pn}_k(X_1,\dots,X_k)\) that express that there is an increasing sequence of points \(t_1,\dots,t_k\) in the unit interval ahead such that \(X_i\) is true at \(t_i\). The logics TLC and TLP have been introduced and studied in earlier work by \textit{Y. Hirshfeld} and \textit{A. Rabinovich} [Lect. Notes Comput. Sci. 1644, 422--432 (1999; Zbl 0939.03023); Log. Methods Comput. Sci. 3, No.~1, Paper 3, 11~p. (2007; Zbl 1128.03007)], where it was shown that TLC and TLP have the same expressive power and are both decidable. The main results of this paper are the exact complexity bounds for the satisfiability problem of TLC and TLP. The satisfiability problem for TLP is PSPACE-complete. The satisfiability problem for TLC is PSPACE-complete if one uses unary coding for the indices of the operators \(C_k\), and it is EXPSPACE-complete if one uses binary coding for these indices.
reviewed by: Clemens Kupke
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 5712829
zbMATH Keywords: temporal logic
zbMATH Keywords: complexity
zbMATH Keywords: expressive power
zbMATH Keywords: satisfiability problems
MaRDI profile type: Publication
full work available at URL: j.tcs.2010.03.017
OpenAlex ID: W2043086238
cites work: The benefits of relaxing punctuality
cites work: Q3835817
cites work: Q4251919
cites work: Q4938638
cites work: Q4945224
cites work: Q4824483
cites work: Timer formulas and decidable metric temporal logic
cites work: An Expressive Temporal Logic for Real Time
cites work: Expressiveness of Metric modalities for continuous time
cites work: Models for reactivity
cites work: Quantitative temporal logics over the reals: PSpace and below
cites work: Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities
DOI: 10.1016/J.TCS.2010.03.017
Recommended article: Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities
Recommended article: Continuous time temporal logic with counting
Recommended article: On the Expressiveness of MTL with Past Operators
Recommended article: Quantitative temporal logics over the reals: PSpace and below
Recommended article: Time-Bounded Verification
Recommended article: Decidable metric logics
Recommended article: Theorem proving for pointwise metric temporal logic over the naturals via translations
Recommended article: Metric Temporal Logic with Counting
Recommended article: Foundations of Software Science and Computation Structures
Recommended article: Revisiting MITL to Fix Decision Procedures
description: scientific article; zbMATH DE number 5712829