B\"uchi-Kamp Theorems for 1-clock ATA
Shankara Narayanan Krishna, Khushraj Madnani, Paritosh Pandya

TL;DR
This paper establishes expressive equivalences between 1-clock alternating timed automata, various timed logics, and MSO fragments, extending classical Kamp theorems to timed automata with new subclasses and logical characterizations.
Contribution
It introduces loop-free-resets and conjunctive-disjunctive subclasses of 1-clock ATA, proving their expressive equivalences with specific timed logics and MSO fragments, extending Kamp-like theorems to timed automata.
Findings
1-ATA with loop-free-resets is equivalent to $ egmtl$.
Subclasses of 1-ATA correspond to fragments of $ egmtl$ and $regmtl$.
Full 1-ATA class matches $ egmtl$ with fixed points.
Abstract
This paper investigates Kamp-like and B\"uchi-like theorems for 1-clock Alternating Timed Automata (1-ATA) and its natural subclasses. A notion of 1-ATA with loop-free-resets is defined. This automaton class is shown to be expressively equivalent to the temporal logic which is extended with a regular expression guarded modality. Moreover, a subclass of future timed MSO with k-variable-connectivity property is introduced as logic . In a Kamp-like result, it is shown that is expressively equivalent to . As our second result, we define a notion of conjunctive-disjunctive 1-clock ATA ( 1-ATA). We show that 1-ATA with loop-free-resets are expressively equivalent to the sublogic of . Moreover is expressively equivalent to , the two-variable connected fragment of . The full…
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.
