Abstract

We describe a decidable class of formulas in a first order timed logic 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. This class covers a wide range of properties arising in the verification of real-time distributed systems with metric time constraints. An important feature of this class is that it makes easy the description of properties of parametric systems, in particular those with real time parameters, with parametric number of processes, and moreover, properties involving arithmetical operations. Another feature of this class is important for the verification: if a formula is not true, then our algorithm gives a quantifier-free description of all counter-models of this formula of the complexity involved in the definition of the decidable class. Such counter-models facilitate the detection of errors in the specifications. Earlier we described decidable classes of verification problems based on a small model property. However, the ‘small models’ that we used were either finite, or similar to those that are introduced in this paper, but without the possibility of treatment of systems with a parametric number of processes.