An Expressive Temporal Logic for Real Time

Abstract. We add to the standard temporal logic with the modalities ”Until ” and ”Since”, a sequence of “counting modalities”: For each n the modality Cn(X), which says that X will be true at least at n points in the next unit of time, and its past counterpart ← − C n, whichsaysthatX has happened at least n times in the last unit of time. We prove that this temporal logic is as expressive as can be hoped for; all the modalities that can be expressed in a strong natural decidable predicate logic framework, are expressible in this temporal logic. 1