文章基本信息

标题：Making Metric Temporal Logic Rational
本地全文：下载
作者：Shankara Narayanan Krishna ; Khushraj Madnani ; Paritosh K. Pandya 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：83
页码：77:1-77:14
DOI：10.4230/LIPIcs.MFCS.2017.77
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We study an extension of MTL in pointwise time with regular expression guarded modality Reg_I(re) where re is a rational expression over subformulae. We study the decidability and expressiveness of this extension (MTL+Ureg+Reg), called RegMTL, as well as its fragment SfrMTL where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that RegMTL has decidable satisfiability by giving an equisatisfiable reduction to MTL. We also identify a subclass MITL+UReg of RegMTL for which our equisatisfiable reduction gives rise to formulae of MITL, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between SfrMTL and partially ordered (or very weak) 1-clock alternating timed automata.
关键词：Metric Temporal Logic; Timed Automata; Regular Expression; Equisatisfiability; Expressiveness