Büchi-Kamp Theorems for 1-clock ATA
share
This paper investigates Kamp-like and Büchi-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 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 . 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 class of 1-ATA is shown to be expressively equivalent to extended with fixed point operators.
READ FULL TEXT