Periodicity based decidable classes in a first order timed logic (Q2368906)

A decidable class of formulas in a first-order timed logic (FOTL) based on a generalized small model property (if a formula has a model then it has a model composed of a finite number of ``ultimately repetitive'' models) is described. It is proved that for a given FOTL formula one can describe all counter-models of a given complexity by a quantifier-free formula in a decidable theory. Such counter-models facilitate the detection of errors in a specification. This class of formulas covers a wide range of properties arising in the verification of real-time distributed systems with metric time constraints and it makes easy the description of properties of parametric systems, in particular those with real-time parameters, with a parametric number of processes and properties involving arithmetical operations.