2026-07-20T12:07:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7912 2024-03-06T10:41:34Z ddc:004 open_access

Timed-Automata-Based Verification of MITL over Signals Brihaye, Thomas Geeraerts, Gilles Ho, Hsi-Ming Monmege, Benjamin real-time temporal logic timed automata real-time systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Brihaye and Gilles Geeraerts and Hsi-Ming Ho and Benjamin Monmege 2017 Is Part Of LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2017.7 urn:nbn:de:0030-drops-79126 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.7 eng https://creativecommons.org/licenses/by/3.0/legalcode