Translating point-in-time Metric Temporal Logic to Timed Automata
Examensarbete för masterexamen
Please use this identifier to cite or link to this item:
Bibliographical item details
|Type: ||Examensarbete för masterexamen|
|Title: ||Translating point-in-time Metric Temporal Logic to Timed Automata|
|Authors: ||Eeten-Jeppsson, Mattis|
|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.|
|Issue Date: ||2021|
|Publisher: ||Chalmers tekniska högskola / Institutionen för data och informationsteknik|
|Collection:||Examensarbeten för masterexamen // Master Theses|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.