Skip to main content

Metric Temporal Logic for Data Words

Karin Quaas ( University of Leipzig )

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.

Speaker bio

I am postdoc in the research group Automata and Formal Languages at the Faculty of Computer Science at the University of Leipzig in Germany. My research interests are real-timed systems and logics, counter automata, and weighted automata. I am also the head of the DFG-funded research project Verification of Weighted Timed Automata and associated member of the DFG research training group Quantitative Logics and Automata.

Share this: