Temporal logics for real-time system specification

The specification of reactive and real-time systems must be supported by fo rmal, mathematically-founded methods in order to be satisfactory and reliab le. Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formu las, including temporal constraints, events, and the relationships between the two. In the last ten years, temporal logics have reached a high degree of expressiveness. Most of the temporal logics proposed in the last few yea rs can be used for specifying reactive systems, although not all are suitab le for specifying real-time systems. In this paper we present a series of c riteria for assessing the capabilities of temporal logics for the specifica tion, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness, the logic's order, presence of a metric fo r time, the type of temporal operators, the fundamental time entity, and th e structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer, a set of typical specificat ions is identified and used with most of the temporal logics considered, th us presenting the reader with a number of real examples.