Continuous time temporal logic with counting

We add to the standard temporal logic TL(U,S) a sequence of "counting modalities": For each n the modality C-n(X), which says that X will be true at least at n points in the next unit of time, and its dual (C) over left arrow (n), which says that X has happened n times in the last unit of time. We show that this temporal logic is expressively complete for the metric predicate logic Q2MLO, which is expressive, decidable and easy to use. In particular the Pnueli modalities P-n (X-1, ... , X-n), "there is an increasing sequence t(1), ... , t(n) of points in the unit interval ahead such that t(i) satisfies X-i", are definable in TL(U,S) with the counting modalities. (C) 2011 Elsevier Inc. All rights reserved.