Logics Meet 2-Way 1-Clock Alternating Timed Automata
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.
Keywords
Cite
@article{arxiv.2107.12986,
title = {Logics Meet 2-Way 1-Clock Alternating Timed Automata},
author = {Shankara Narayanan Krishna and Khushraj Nanik Madnani and Manuel Mazo and Paritosh K. Pandya},
journal= {arXiv preprint arXiv:2107.12986},
year = {2022}
}
Comments
arXiv admin note: text overlap with arXiv:2105.09534