B\"uchi-Kamp Theorems for 1-clock ATA

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 $\regmtl$ which is $\mathsf{MTL[F_I]}$ extended with a regular expression guarded modality. Moreover, a subclass of future timed MSO with k-variable-connectivity property is introduced as logic $\qkmso$. In a Kamp-like result, it is shown that $\regmtl$ is expressively equivalent to $\qkmso$. As our second result, we define a notion of conjunctive-disjunctive 1-clock ATA ($\wf$ 1-ATA). We show that $\wf$ 1-ATA with loop-free-resets are expressively equivalent to the sublogic $\F\regmtl$ of $\regmtl$. Moreover $\F\regmtl$ is expressively equivalent to $\qtwomso$, the two-variable connected fragment of $\qkmso$. The full class of 1-ATA is shown to be expressively equivalent to $\regmtl$ extended with fixed point operators.