In automata theory, an alternating timed automaton (ATA) is a mix of both timed automaton and alternating finite automaton. That is, it is a sort of automata which can measure time and in which there exists universal and existential transition.
ATAs are more expressive than timed automaton. one clock alternating timed automaton (OCATA) is the restriction of ATA allowing the use of a single clock. OCATAs allow to express timed languages which can not be expressed using timed-automaton.[1]
An alternating timed automaton is defined as a timed automaton, where the transitions are more complex.
Given a set
X
lB+(X)
X
X
\phi\land\psi
\phi\lor\psi
\phi,\psi\inlB+(X)
For each letter
a
\ell
lBa,\ell
|X| | |
R | |
\ge0 |
|X|
\nu
c(a,\ell,\nu)
lBa,\ell
\nu
An alternating timed-automaton contains a transition function, which associates to a 3-tuple
(\ell,a,c)
c\inlBa,\ell
lB+(L x lP(C))
For example,
(\ell1,\emptyset)\lor((\ell2,\{x\})\land(\ell2,\{y\}))
lB+(L x lP(C))
\ell1
\ell2
x
y
Formally, an alternating timed automaton is a tuple
lA=\langle\Sigma,L,L0,C,F,E\rangle
lA
L
L
lA
C
lA
L0\subseteqL
F\subseteqL
E\subseteqL x \Sigma x lB(C)\tolB+(L x lP(C))
lA
Any Boolean expression can be rewritten into an equivalent expression in disjunctive normal form. In the representation of a 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. The tail is labelled by the letter and each head is labelled by the set of clocks it resets.
We now define a run of an alternating timed automaton over a timed word
w=(\sigma1,t1),(\sigma2,t2),...,
In this definition of a run, a run is not anymore a list of pairs, but a rooted tree. The node of the trooted tree are labelled by pairs with a location and a clock valuation. The tree is defined as follows:
(\ell0,\nu0)
\ell0\inL0
n
i
(\ell,\nu)
E(ai+1,\ell,c(a,\ell,\nu))
mi | |
vee | |
j=1 |
(\elli,j,ri,j)
n
mi
1\lei\len
j
(\elli,j,(\nu+ti+1-ti)[ri,j\to0]
The definition of an accepting runs differs depending on whether the timed word is finite or infinite. If the timed word is finite, then the run is accepting if the label of each leaf contains an accepting location. If the timed word is infinite, then a run is accepting if each branch contains an infinite number of accepting location.
A run can also be defined as a two player game
GA,w
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
lB+(L x lP(C))
(\ell,\nu,i,b)
i
\ell
\nu
b
(\ell0,\nu0,0)
\ell0\inL0
(\ell,\nu,i)
i
(\ell,\nu,i,c(ai+1,\ell,\nu))
(\ell,\nu,i,(\ell',r))
(\ell',\nu+ti-ti-1[r\to0],i+1)
(\ell,\nu,i,\phi\lor\psi)
(\ell,\nu,i,\phi)
(\ell,\nu,i,\psi)
(\ell,\nu,i,\phi\land\psi)
(\ell,\nu,i,\phi)
(\ell,\nu,i,\psi)
The set of successive states starting in a state of the form
(\ell,\nu,i)
The definition of an accepting run is the same than for timed automata.
A one clock alternating timed automaton (OCATA) is an alternating timed automaton using a single clock.
The expressivity of OCATAs and of timed-automaton are incomparable.
For example, the language over the alphabet
\{a\}
x
x
An ATA is said to be purely-universal (respectively, purely-exisential) 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.
Given an ATA
lA=\langle\Sigma,L,\{q0\},C,F,E\rangle
L
Lc
Ac
\langle\Sigma,L,\{q0\},C,L\setminusF,E'\rangle
E'(\ell,a,c)
E(\ell,a,c))
E'(q0,a,c)
L0
It follows that the class of language accepted by ATAs and by OCATAs are accepted by unions and intersection. The union of two languages is constructed by taking disjoint copies of the automata accepting both language. The intersection can be constructed from union and concatenation.
The emptiness problem, the universality problem and the containability problem for OCATA is decidable but is a nonelementary problem.
Those three problems are undecidable over ATAs.