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:
Download file(s):
File Description SizeFormat 
CSE 21-118 Eeten-Jeppsson.pdf1.36 MBAdobe PDFView/Open
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.