Alternating timed automaton explained

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]

Definition

An alternating timed automaton is defined as a timed automaton, where the transitions are more complex.

Difference from a timed-automaton

Given a set

X

, let

lB+(X)

the set of positive Boolean combination of elements of

X

. I.e. the set containing the elements of

X

, and containing

\phi\land\psi

and

\phi\lor\psi

, for

\phi,\psi\inlB+(X)

.

For each letter

a

and location

\ell

, let

lBa,\ell

be a set of clock constraints such that their zones partition
|X|
R
\ge0
, with

|X|

the number of clocks. Given a clock valuation

\nu

, let

c(a,\ell,\nu)

be the only clock constraint of

lBa,\ell

which is satisfied by

\nu

.

An alternating timed-automaton contains a transition function, which associates to a 3-tuple

(\ell,a,c)

, with

c\inlBa,\ell

, to an element of

lB+(L x lP(C))

.

For example,

(\ell1,\emptyset)\lor((\ell2,\{x\})\land(\ell2,\{y\}))

is an element of

lB+(L x lP(C))

. Intuitively, it means that the run may either continue by moving to location

\ell1

, and resetting no clock. Or by moving to location

\ell2

and should be successful when either

x

or

y

is reset.

Formal definition

Formally, an alternating timed automaton is a tuple

lA=\langle\Sigma,L,L0,C,F,E\rangle

that consists of the following components:

lA

.

L

is a finite set. The elements of

L

are called the locations or states of

lA

.

C

is a finite set called the clocks of

lA

.

L0\subseteqL

is the set of start locations.

F\subseteqL

is the set of accepting locations.

E\subseteqL x \Sigma x lB(C)\tolB+(L x lP(C))

is the transitions function of

lA

. It is a partial function, defined as explained in the previous section.

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.

Run

We now define a run of an alternating timed automaton over a timed word

w=(\sigma1,t1),(\sigma2,t2),...,

. There are two equivalent way to define a run, either as a tree or as a game.

Run as a tree

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)

with

\ell0\inL0

,

n

of the tree at depth

i

, with label

(\ell,\nu)

. Without loss of generality, let us assume that

E(ai+1,\ell,c(a,\ell,\nu))

is in disjunctive normal form, i.e. it is of the form
mi
vee
j=1

(\elli,j,ri,j)

. Then the node

n

has

mi

children, for some

1\lei\len

. The

j

-th child is labelled by

(\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.

Run as a game

A run can also be defined as a two player game

GA,w

. Let us call the two players "player" and "opponent". 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

lB+(L x lP(C))

. Intuitively, a tuple

(\ell,\nu,i,b)

means that the run has read

i

letters, is in location

\ell

, with clock value

\nu

, and that the transition will be as described by

b

. The run is defined as follow:

(\ell0,\nu0,0)

, for some

\ell0\inL0

.

(\ell,\nu,i)

, if the length of the word is

i

, the run ends. Otherwise, its successor state is

(\ell,\nu,i,c(ai+1,\ell,\nu))

.

(\ell,\nu,i,(\ell',r))

is the state

(\ell',\nu+ti-ti-1[r\to0],i+1)

,

(\ell,\nu,i,\phi\lor\psi)

is chosen by the player, it is either

(\ell,\nu,i,\phi)

or

(\ell,\nu,i,\psi)

,

(\ell,\nu,i,\phi\land\psi)

is chosen by the opponent, it is either

(\ell,\nu,i,\phi)

or

(\ell,\nu,i,\psi)

.

The set of successive states starting in a state of the form

(\ell,\nu,i)

and ending in before the next such state is called a phase.

The definition of an accepting run is the same than for timed automata.

Subclass of ATA

One clock alternating timed automaton

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\}

such that there is never exactly one time unit between two letters can not be recognized by a timed-automaton. However, the OCATA pictured nearby accepts it. In this alternating timed automaton, two branches are started. A branch restarts the clock

x

, and ensures that each time in the future when a letter is emitted, the clock

x

is distinct from 1. This ensure that between this letter and the next ones, the time elapsed is not one. The second branch only waits for other letters to be emitted and do the same checking.

Purely-Universal and Purely-Existential ATA

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.

Closure

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

accepting a timed language

L

, its complement language

Lc

is accepted by an automaton

Ac

which is essentially

\langle\Sigma,L,\{q0\},C,L\setminusF,E'\rangle

, where

E'(\ell,a,c)

is defined as

E(\ell,a,c))

where disjunction and conjunctions are reversed and

E'(q0,a,c)

simulates the run from each of the locations of

L0

simultaneously.

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.

Complexity

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.

Notes and References

  1. Lasota . SƗawomir . Walukiewicz . Igor . Alternating Timed Automata . ACM Transactions on Computational Logic . 2008 . 9 . 2 . 1–26 . 10.1145/1342991.1342994. 1208.5909 . 12319 .