Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities

The common metric temporal logics for continuous time were shown to be insufficient, when it was proved in [7, 12] that they cannot express a modality suggested by Pnueli. Moreover no temporal logic with a finite set of modalities can express all the natural generalizations of this modality. The temporal logic with counting modalities (TLC) is the extension of until-since temporal logic TL(U, S) by "counting modalities" Cn(X) and C n (n N); for each n the modality Cn(X) says that X will be true at least at n points in the next unit of time, and its dual C n(X) says that X has happened n times in the last unit of time. In [11] it was proved that this temporal logic is expressively complete for a natural decidable metric predicate logic. In particular the Pnueli modalities Pnk(X1, . . . , Xk), "there is an increasing sequence t1, . . . , tk of points in the unit interval ahead such that Xi holds at ti", are definable in TLC. In this paper we investigate the complexit...

• Type: Conference
• Year: 2008
• Where: FORMATS
• Authors: Alexander Rabinovich
• Keywords: Formal Methods, FORMATS 2008, Metric Temporal Logics, Temporal Logic, Until-since Temporal Logic