Metric Temporal Logic for Data Words

Linear time temporal logic (LTL) is nowadays one of the main logical formalisms used for the specification and verification of reactive systems, and has found many useful applications in industrial tools. On the negative side, LTL provides only limited possibilities to express quantitative information, like, e.g., "from now on in 20 seconds the alarm will go off", or "the value of this stock will never go below 30 Dollars". In this talk, we consider Metric Temporal Logic (MTL), an extension of LTL, which may be used to express such quantitative properties. In MTL, temporal modalities (like Until, Next, Finally, or Globally) may be indexed with an interval that, additionally to the usual semantics of LTL formulae, determines the data values that have to hold in a model. The above two properties, for instance, may be expressed in MTL by the formulae $F_{[20,20]}alarm$ and $G_{[0,30)} false$. MTL was originally introduced to express real-time properties, and the complexity of various important verification problems like satisfiability, model- and path checking are well known for a while now. In the talk, I will report on recent results on these verifications problems for a setting in which data values may - in contrast to the real-timed setting - increase and decrease with time.