Alternating timed automaton
An alternating timed automaton[1] (ATA) is a modeling formalism that combines features of timed automaton[2] and an alternating finite automaton[3] to succinctly express sets of timed event sequences.
Classical timed automata only allow existential nondeterministic branching in their transitions, while alternating finite automata model discrete untimed behaviors.
However, this increased expressive power comes at the cost of undecidability in their emptiness problem.
During a run of a timed automaton, clock values increase all with the same speed.
Along the transitions of the automaton, clock values can be compared to integers.
These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviors of the automaton are more expressive than timed automata.
be the set of positive Boolean combination of elements of
be a set of clock constraints such that their zones partition
An alternating timed-automaton contains a transition function, which associates to a 3-tuple
characterizing a condition over next locations and clocks to be reset.
Intuitively, this means that a run (or, execution) of the automaton may existentially branch into two possibilities: 1) continue by moving to location
without resetting any clock, or 2) universally branch into two possibilities, both moving to location
Formally, an alternating timed automaton is a tuple
In the representation of an ATA, each disjunction is represented by a different arrow.
Each conjunct of a disjunction is represented by a set of arrows with the same tail and multiple heads.
can be defined in one of two equivalent ways: as a tree or as a game.
[citation needed] In this definition, a run is not merely a list of pairs, but a rooted tree.
The nodes of the rooted tree are labelled by pairs with a location and a clock valuation.
The tree is defined as follows: The definition of an accepting run differs depending on whether the timed word is finite or infinite.
The goal of the player is to create an accepting run, and the goal of the opponent is to create a rejecting (non-accepting) run.
Each state of the game is a tuple composed of a location, a clock valuation, a position in the word, and potentially an element of
The definition of an accepting run is the same as that for timed automata.
such that there is never exactly one time unit between two letters can not be recognized by a timed-automaton.
In this alternating timed automaton, two branches are started.
, and ensures that each time in the future when a letter is emitted, the clock
The second branch only waits for other letters to be emitted and does the same checking.
An ATA is said to be purely-universal (respectively, purely-existential) if its transition function does not use disjunction (respectively, conjunction).
Purely-existential ATAs are as expressive as non-deterministic timed-automaton.
The class of language accepted by ATAs and by OCATAs is closed under complement.
The construction is explained for the case where there is a single initial location.
