Complexity of metric temporal logics with counting and the Pnueli modalities (Q974119): Difference between revisions

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.