Logics Meet 2-Way 1-Clock Alternating Timed Automata

TL;DR

This paper extends 1-clock Alternating Timed Automata to include two-way reading capabilities, explores their expressiveness, and introduces restrictions that make emptiness checking decidable with elementary complexity.

Contribution

It introduces 2-Way 1-ATA with reset-free loops, establishes their expressive equivalence to GQMSO, and proposes a non-adjacency restriction for decidability.

Findings

2-Way 1-ATA with reset-free loops is expressively equivalent to GQMSO.

Decidability of emptiness checking is achieved under non-adjacency restrictions.

Non-Adjacent 2-Way 1-ATA is the first class with decidable emptiness among timed automata with two-wayness and alternations.

Abstract

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.