2026-08-18T16:42:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9577 2024-03-06T10:44:46Z ddc:004 open_access

Logics Meet 1-Clock Alternating Timed Automata Krishna, Shankara Narayanan Madnani, Khushraj Pandya, Paritosh K. Metric Temporal Logic Alternating Timed Automata MSO Regular Expressions Expressive Completeness 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Shankara Narayanan Krishna and Khushraj Madnani and Paritosh K. Pandya 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.39 urn:nbn:de:0030-drops-95779 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.39 eng https://creativecommons.org/licenses/by/3.0/legalcode