We add to the standard temporal logic with the modalities "Until" and "Since", 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 past counterpart C_n, which says that X 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.
展开▼
