文章基本信息

标题：Timed-Automata-Based Verification of MITL over Signals
本地全文：下载
作者：Thomas Brihaye ; Gilles Geeraerts ; Hsi-Ming Ho 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：90
页码：7:1-7:19
DOI：10.4230/LIPIcs.TIME.2017.7
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：real-time temporal logic; timed automata; real-time systems