Specifying real-time properties with metric temporal logic

R Koymans - Real-time systems, 1990 - Springer
R Koymans
Real-time systems, 1990Springer
This paper is motivated by the need for a formal specification method for real-time systems.
In these systems quantitative temporal properties play a dominant role. We first characterize
real-time systems by giving a classification of such quantitative temporal properties. Next, we
extend the usual models for temporal logic by including a distance function to measure time
and analyze what restrictions should be imposed on such a function. Then we introduce
appropriate temporal operators to reason about such models by turning qualitative temporal …
Abstract
This paper is motivated by the need for a formal specification method for real-time systems. In these systemsquantitative temporal properties play a dominant role. We first characterize real-time systems by giving a classification of such quantitative temporal properties. Next, we extend the usual models for temporal logic by including a distance function to measure time and analyze what restrictions should be imposed on such a function. Then we introduce appropriate temporal operators to reason about such models by turning qualitative temporal operators into (quantitative) metric temporal operators and show how the usual quantitative temporal properties of real-time systems can be expressed in this metric temporal logic. After we illustrate the application of metric temporal logic to real-time systems by several examples, we end this paper with some conclusions.
Springer