Translating point-in-time Metric Temporal Logic to Timed Automata

Abstract

Metric Temporal Logic (MTL) extends the modalities of LTL with timing, making it well suited for specifying properties over real timed traces. This thesis is concerned with applying MTL to runtime verification with the purpose of obtaining a monitoring procedure based on timed automata. Target semantics are stated which are weak and strong truncated paths semantics for point-in-time MTL and which give a verdict for every finite or infinite trace. While these semantics clearly state our intention they are impractical for our purposes and we give equivalent unified semantics based on extending finite paths with “all true” and “all false”. This is the first such treatment given for the point-in-time domain. An existing construction based on timed automata is then adapted to implement the target semantics and is extended with the past fragment of MTL. Finally it is shown how this construction can be applied to monitoring.