On the expressiveness of metric temporal logic

Abstract

Temporal Logics are a popular formalism for specification of properties in the verification of reactive systems. They can be employed to reason about the behavior of systems with the evolution of time. For example, one can specify that an event corresponding to the request of a resource is eventually followed by an event corresponding to its grant. Linear-time Temporal Logic (LTL) is one such formalism which, apart from its applications in verification, has strong theoretical links with other well-known logic and automata-based formalisms. Though it can be used to specify a wide range of qualitative behaviors of systems, like the example above, it does not suffice to verify quantitative properties which have explicit references to the times of occurrences of events. Such properties are common in real-time systems, which have strict real-time constraints, like a request should be satisfied within 5 time units. Metric Temporal Logic (MTL) is an extension of LTL to verify real-time properties. In this thesis, we study issues related to the expressiveness of MTL. There have been two ways in which the formulas in the logic have been interpreted in the literature, which have come to be known as the “pointwise” and “continuous” semantics. In the pointwise semantics, one can assert a property only at the action points corresponding to the occurrence of events, whereas in the continuous semantics, a property can be asserted at any real-time point. In this thesis, we compare the expressiveness of MTL with respect to the two semantics for its various syntactic variants. We also give a characterization of the languages definable in MTL in terms of a necessary “counter-freeness” property. Finally, we show that MTL is expressively complete in that there are natural logics characterizing it.