Alternating timed automaton

In automata theory, a timed automaton is a finite automaton extended with a finite set of real-valued clocks. 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.

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

Given a set $X$, let $\backslash mathcal\; B^+(X)$ be the set of positive Boolean combination of elements of $X$, i.e. the set containing the elements of $X$, and containing $\backslash phi\backslash land\backslash psi$ and $\backslash phi\backslash lor\backslash psi$, for $\backslash phi,\backslash psi\backslash in\backslash mathcal\; B^+(X)$.

For each letter $a$ and location $\backslash ell$, let $\backslash mathcal\; B\_\{a,\backslash ell\}$ be a set of clock constraints such that their zones partition $\backslash mathbb\; R\_\{\backslash ge\; 0\}^$

An alternating timed-automaton contains a transition function, which associates to a 3-tuple $(\backslash ell,a,c)$, with $c\backslash in\backslash mathcal\; B\_\{a,\backslash ell\}$, to an element of $\backslash mathcal\; B^+(L\backslash times\backslash mathcal\; P(C))$.

For example, $(\backslash ell\_1,\backslash emptyset)\backslash lor((\backslash ell\_2,\backslash \{x\backslash \})\backslash land(\backslash ell\_2,\backslash \{y\backslash \}))$ is an element of $\backslash mathcal\; B^+(L\backslash times\backslash mathcal\; P(C))$ 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 $\backslash ell\_1$without resetting any clock, or 2) universally branch into two possibilities, both moving to location $\backslash ell\_2$ with one resetting clock $x$ and the other resetting clock $y$.

Formally, an alternating timed automaton is a tuple $\backslash mathcal\; A=\backslash langle\; \backslash Sigma,L,L\_0,C,F,E\backslash rangle$ that consists of the following components:

• Σ is a finite set called the alphabet or actions of $\backslash mathcal\; A$.
• $L$ is a finite set. The elements of $L$ are called the locations or states of $\backslash mathcal\; A$.
• $C$ is a finite set called the clocks of $\backslash mathcal\; A$.
• $L\_0\backslash subseteq\; L$ is the set of start locations.
• $F\backslash subseteq\; L$ is the set of accepting locations.
• $E\backslash subseteq\; L\backslash times\backslash Sigma\backslash times\backslash mathcal\; B(C)\backslash to\backslash mathcal\; B^+(L\backslash times\; \backslash mathcal\; P(C))$ is the transitions function of $\backslash mathcal\; A$.

Any Boolean expression can be rewritten into an equivalent expression in disjunctive normal form. 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. The tail is labelled by the letter and each head is labelled by the set of clocks it resets{{Example needed|date=September 2024}}.

A run of an alternating timed automaton over a timed word $w=(\backslash sigma\_1,t\_1),(\backslash sigma\_2,t\_2),\backslash dots$ can be defined in one of two equivalent ways: as a tree or as a game.{{Citation needed|date=September 2024}}

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 root of the tree is of the form $(\backslash ell\_0,\backslash nu\_0)$ with $\backslash ell\_0\backslash in\; L\_0$,
• Consider a node $n$ of the tree at depth $i$, with label $(\backslash ell,\backslash nu)$. Without loss of generality, let us assume that $E(a\_\{i+1\},\backslash ell,c(a,\backslash ell,\backslash nu))$ is in disjunctive normal form, i.e. it is of the form $\backslash bigvee\_\{i=1\}^n\backslash bigwedge\_\{j=1\}^\{m\_i\}(\backslash ell\_\{i,j\},\; r\_\{i,j\})$. Then the node $n$ has $m\_i$ children, for some $1\backslash le\; i\backslash le\; n$. The $j$-th child is labelled by $(\backslash ell\_\{i,j\},(\backslash nu+t\_\{i+1\}-t\_\{i\})[r\_\{i,j\}\backslash to\; 0]$.

The definition of an accepting run 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 locations.

A run can also be defined as a two player game $G\_\{A,w\}$, with the two players called "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 $\backslash mathcal\; B^+(L\backslash times\backslash mathcal\; P(C))$. Intuitively, a tuple $(\backslash ell,\backslash nu,i,b)$ means that the run has read $i$ letters, is in location $\backslash ell$, with clock value $\backslash nu$, and that the transition will be as described by $b$. The run is defined as follows:

• The initial state is of the form $(\backslash ell\_0,\backslash nu\_0,\; 0)$, for some $\backslash ell\_0\backslash in\; L\_0$.
• Given a state $(\backslash ell,\backslash nu,i)$, if the length of the word is $i$, the run ends. Otherwise, its successor state is $(\backslash ell,\backslash nu,i,c(a\_\{i+1\},\backslash ell,\backslash nu))$.
• The successor of a state $(\backslash ell,\backslash nu,i,(\backslash ell\text{'},r))$ is the state $(\backslash ell\text{'},\backslash nu+t\_\{i\}-t\_\{i-1\}[r\backslash to0],i+1)$,
• The successor of a state $(\backslash ell,\backslash nu,i,\backslash phi\backslash lor\backslash psi)$ is chosen by the player, it is either $(\backslash ell,\backslash nu,i,\backslash phi)$ or $(\backslash ell,\backslash nu,i,\backslash psi)$,
• The successor of a state $(\backslash ell,\backslash nu,i,\backslash phi\backslash land\backslash psi)$ is chosen by the opponent, it is either $(\backslash ell,\backslash nu,i,\backslash phi)$ or $(\backslash ell,\backslash nu,i,\backslash psi)$.

The set of successive states starting in a state of the form $(\backslash ell,\backslash nu,i)$ and ending before the next such state is called a phase.

The definition of an accepting run is the same as that 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-automata are incomparable.{{Clarify|date=September 2024}}

For example, the language over the alphabet $\backslash \{a\backslash \}$ such that there is never exactly one time unit between two letters can not be recognized by a timed-automaton. However, the OCATA pictured 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 does the same checking.

File:2019-03-31-213847 313x156 scrot.png

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.

Given an ATA $\backslash mathcal\; A=\backslash langle\; \backslash Sigma,L,\backslash \{q\_0\backslash \},C,F,E\backslash rangle$ accepting a timed language $L$, its complement language $L^c$ is accepted by an automaton $A^c$ which is essentially $\backslash langle\; \backslash Sigma,L,\backslash \{q\_0\backslash \},C,L\backslash setminus\; F,E\text{'}\backslash rangle$, where $E\text{'}(\backslash ell,a,c)$ is defined as $E(\backslash ell,a,c))$ where disjunction and conjunctions are reversed and $E\text{'}(q\_0,a,c)$ simulates the run from each of the locations of $L\_0$ 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 languages. The intersection can be constructed from union and concatenation.

The emptiness problem, the universality problem and the containability problem are undecidable for ATAs, but decidable for OCATAs, though it{{Ambiguous|date=September 2024}} is a nonelementary problem.

{{Reflist}}

Category:Automata (computation)

Category:Model checking