Timer formulas and decidable metric temporal logic (Q1780454)

A quantitative temporal logic is defined that is based on a simple modality within the framework of monadic predicate logic. Its canonical model is the real line. It can be interpreted either by behavior with finite variability or by unrestricted behavior. In both cases decidability and complexity bounds are proved using general theorems from logic. The 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.