Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2017.7
URN: urn:nbn:de:0030-drops-79126
URL: https://drops.dagstuhl.de/opus/volltexte/2017/7912/
Brihaye, Thomas ; Geeraerts, Gilles ; Ho, Hsi-Ming ; Monmege, Benjamin
Timed-Automata-Based Verification of MITL over Signals
| pdf-format: |
|
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: | 25.09.2017 |
