eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-08-31
39:1
39:17
10.4230/LIPIcs.CONCUR.2018.39
article
Logics Meet 1-Clock Alternating Timed Automata
Krishna, Shankara Narayanan
1
Madnani, Khushraj
1
Pandya, Paritosh K.
2
Department of Computer Science & Engineering IIT Bombay, India
School of Technology and Computer Science, TIFR, India
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol118-concur2018/LIPIcs.CONCUR.2018.39/LIPIcs.CONCUR.2018.39.pdf
Metric Temporal Logic
Alternating Timed Automata
MSO
Regular Expressions
Expressive Completeness