Alternating Timed Automata
Slawomir Lasota, Igor Walukiewicz

TL;DR
This paper introduces alternating timed automata with one clock, demonstrating their decidable emptiness problem over finite words, and explores extensions leading to undecidability results for infinite words.
Contribution
It proposes a new class of alternating timed automata with decidable emptiness and analyzes their computational complexity and extensions.
Findings
Decidability of emptiness for automata with one clock over finite words
Non-primitive recursive complexity of the emptiness problem
Undecidability results for extensions and infinite words
Abstract
A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages which is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is non-primitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock. We investigate extension of the model with epsilon-transitions and prove that emptiness is undecidable. Over infinite words, we show undecidability of the universality problem.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Petri Nets in System Modeling
