تقرير
Logics Meet 2-Way 1-Clock Alternating Timed Automata
| العنوان: | Logics Meet 2-Way 1-Clock Alternating Timed Automata |
|---|---|
| المؤلفون: | Krishna, Shankara Narayanan, Madnani, Khushraj Nanik, Mazo Jr., Manuel, Pandya, Paritosh K. |
| سنة النشر: | 2021 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Formal Languages and Automata Theory, Computer Science - Logic in Computer Science, F.4.3, F.4.1, F.1.1 |
| الوصف: | 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. Comment: arXiv admin note: text overlap with arXiv:2105.09534 |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2107.12986 |
| رقم الأكسشن: | edsarx.2107.12986 |
| قاعدة البيانات: | arXiv |
كن أول من يترك تعليقا!