Timer formulas and decidable metric temporal logic

We define a quantitative temporal logic that is based on a simple modality within the framework of monadic predicate logic. Its canonical model is the real line (and not an ω-sequence of some type). It can be interpreted either by behaviors with finite variability or by unrestricted behaviors. For finite variability models it is as expressive as any logic suggested in the literature. For unrestricted behaviors our treatment is new. In both cases we prove decidability and complexity bounds using general theorems from logic (and not from automata theory). The technical proof uses a sublanguage of the metric monadic logic of order, the language of timer normal form formulas. Metric formulas are reduced to timer normal form and timer normal form formulas allow elimination of the metric.