文章基本信息

标题：Logics Meet 1-Clock Alternating Timed Automata
本地全文：下载
作者：Shankara Narayanan Krishna ; Khushraj Madnani ; Paritosh K. Pandya 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：118
页码：1-17
DOI：10.4230/LIPIcs.CONCUR.2018.39
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：This paper investigates a decidable and highly expressive real time logic QkMSO which is obtained by extending MSO[<] with guarded quantification using block of less than k metric quantifiers. The resulting logic is shown to be expressively equivalent to 1-clock ATA where loops are without clock resets, as well as, RatMTL, a powerful extension of MTL[U_I] with regular expressions. We also establish 4-variable property for QkMSO and characterize the expressive power of its 2-variable fragment. Thus, the paper presents progress towards expressively complete logics for 1-clock ATA.
关键词：Metric Temporal Logic; Alternating Timed Automata; MSO; Regular Expressions; Expressive Completeness