  In this paper, we study the extension of 1-clock Alternating Timed Automata
(1-ATA) with the ability to read in both forward and backward direction, the
2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that 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).
Emptiness Checking problem for 2-Way 1-ATA-rfl (and hence GQMSO) is
undecidable, in general. We propose a "non-punctuality" like 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 is the first such class of Timed Automata with
alternations and 2-wayness for which the emptiness checking is decidable (and
that too with elementary complexity). We also show that 2-Way 1-ATA-rfl, even
with the non-adjacent restrictions, can express properties is not recognizable
using 1-ATA.
