Brihaye, Thomas ;
Geeraerts, Gilles ;
Ho, Hsi-Ming ;
Monmege, Benjamin
Timed-Automata-Based Verification of MITL over Signals
Abstract
It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i.e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i.e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.
BibTeX - Entry
@InProceedings{brihaye_et_al:LIPIcs:2017:7912,
author = {Thomas Brihaye and Gilles Geeraerts and Hsi-Ming Ho and Benjamin Monmege},
title = {{Timed-Automata-Based Verification of MITL over Signals}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Sven Schewe and Thomas Schneider and Jef Wijsen},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7912},
URN = {urn:nbn:de:0030-drops-79126},
doi = {10.4230/LIPIcs.TIME.2017.7},
annote = {Keywords: real-time temporal logic, timed automata, real-time systems}
}
|
Keywords: |
|
real-time temporal logic, timed automata, real-time systems |
|
Seminar: |
|
24th International Symposium on Temporal Representation and Reasoning (TIME 2017)
|
|
Issue date: |
|
2017 |
|
Date of publication: |
|
2017 |
2017
