2-Way 1-Clock ATA & Its Logics: Back To The Future With Alternations

In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to scan the timed behaviour in both forward and backward directions: the 2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that the subclass of 2-Way 1-ATA with reset free loops (2-Way 1-ATA-rfl) is expressively equivalent to MSO[<] extended with Guarded Metric Quantifiers (GQMSO). The emptiness checking problem for 2-Way 1-ATA-rfl (and hence GQMSO) is undecidable, in general. We propose a generalization of the classical nonpunctuality restriction, called non-adjacency, for 2-Way 1-ATA-rfl, and also for GQMSO, for which the emptiness (respectively, satisfiability) checking becomes decidable. Non-Adjacent 2-Way 1-ATA-rfl is the first class of timed automata with alternations and 2-wayness for which the emptiness checking is decidable with elementary complexity. We also show that 2-Way 1-ATA-rfl, even with the non-adjacent restrictions, can express properties that are not recognizable by 1-ATA.