Alternating timed automaton

Last updated October 23, 2024

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. Unlike timed automata, alternating timed automata are closed under complementation. However, this increased expressive power comes at the cost of undecidability in their emptiness problem.^[1] A one clock alternating timed automaton (OCATA) is a restricted version of an ATA, limited to the use of a single clock. OCATAs can express timed languages that cannot be expressed using standard timed automata.^[1]

Definition

In automata theory, a timed automaton^[2] 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.^[1]

Difference from a timed-automaton

Given a set $X$ , let ${\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 $\phi \land \psi$ and $\phi \lor \psi$ , for $\phi ,\psi \in {\mathcal {B}}^{+}(X)$ .

For each letter $a$ and location $\ell$ , let ${\mathcal {B}}_{a,\ell }$ be a set of clock constraints such that their zones partition $\mathbb {R} _{\geq 0}^{|X|}$ , with $|X|$ being the number of clocks. Given a clock valuation $\nu$ , let $c(a,\ell ,\nu )$ be the only clock constraint of ${\mathcal {B}}_{a,\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\in {\mathcal {B}}_{a,\ell }$ , to an element of ${\mathcal {B}}^{+}(L\times {\mathcal {P}}(C))$ .

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

Formal definition

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

Σ is a finite set called the alphabet or actions of ${\mathcal {A}}$ .
$L$ is a finite set. The elements of $L$ are called the locations or states of ${\mathcal {A}}$ .
$C$ is a finite set called the clocks of ${\mathcal {A}}$ .
$L_{0}\subseteq L$ is the set of start locations.
$F\subseteq L$ is the set of accepting locations.
$E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\to {\mathcal {B}}^{+}(L\times {\mathcal {P}}(C))$ is the transitions function of ${\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 ]}.

Run

A run of an alternating timed automaton over a timed word $w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots$ can be defined in one of two equivalent ways: as a tree or as a game.^{[ citation needed ]}

Run as a tree

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 $(\ell _{0},\nu _{0})$ with $\ell _{0}\in L_{0}$ ,
Consider a node $n$ of the tree at depth $i$ , with label $(\ell ,\nu )$ . Without loss of generality, let us assume that $E(a_{i+1},\ell ,c(a,\ell ,\nu ))$ is in disjunctive normal form, i.e. it is of the form $\bigvee _{i=1}^{n}\bigwedge _{j=1}^{m_{i}}(\ell _{i,j},r_{i,j})$ . Then the node $n$ has $m_{i}$ children, for some $1\leq i\leq n$ . The $j$ -th child is labelled by $(\ell _{i,j},(\nu +t_{i+1}-t_{i})[r_{i,j}\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.

Run as a game

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 ${\mathcal {B}}^{+}(L\times {\mathcal {P}}(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 follows:

The initial state is of the form $(\ell _{0},\nu _{0},0)$ , for some $\ell _{0}\in L_{0}$ .
Given a state $(\ell ,\nu ,i)$ , if the length of the word is $i$ , the run ends. Otherwise, its successor state is $(\ell ,\nu ,i,c(a_{i+1},\ell ,\nu ))$ .
The successor of a state $(\ell ,\nu ,i,(\ell ',r))$ is the state $(\ell ',\nu +t_{i}-t_{i-1}[r\to 0],i+1)$ ,
The successor of a state $(\ell ,\nu ,i,\phi \lor \psi )$ is chosen by the player, it is either $(\ell ,\nu ,i,\phi )$ or $(\ell ,\nu ,i,\psi )$ ,
The successor of a state $(\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 before the next such state is called a phase.

The definition of an accepting run is the same as that 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-automata are incomparable.^{[ clarification needed ]}

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

Purely-Universal and Purely-Existential ATA

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.

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 ${\mathcal {A}}=\langle \Sigma ,L,\{q_{0}\},C,F,E\rangle$ accepting a timed language $L$ , its complement language $L^{c}$ is accepted by an automaton $A^{c}$ which is essentially $\langle \Sigma ,L,\{q_{0}\},C,L\setminus F,E'\rangle$ , where $E'(\ell ,a,c)$ is defined as $E(\ell ,a,c))$ where disjunction and conjunctions are reversed and $E'(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.

Complexity

The emptiness problem, the universality problem and the containability problem are undecidable for ATAs, but decidable for OCATAs, though it^{[ ambiguous ]} is a nonelementary problem.

Related Research Articles

In particle physics, the Dirac equation is a relativistic wave equation derived by British physicist Paul Dirac in 1928. In its free form, or including electromagnetic interactions, it describes all spin-1/2 massive particles, called "Dirac particles", such as electrons and quarks for which parity is a symmetry. It is consistent with both the principles of quantum mechanics and the theory of special relativity, and was the first theory to account fully for special relativity in the context of quantum mechanics. It was validated by accounting for the fine structure of the hydrogen spectrum in a completely rigorous way. It has become vital in the building of the Standard Model.

Noether's theorem states that every continuous symmetry of the action of a physical system with conservative forces has a corresponding conservation law. This is the first of two theorems published by mathematician Emmy Noether in 1918. The action of a physical system is the integral over time of a Lagrangian function, from which the system's behavior can be determined by the principle of least action. This theorem only applies to continuous and smooth symmetries of physical space.

The Fock space is an algebraic construction used in quantum mechanics to construct the quantum states space of a variable or unknown number of identical particles from a single particle Hilbert space $H$ . It is named after V. A. Fock who first introduced it in his 1932 paper "Konfigurationsraum und zweite Quantelung".

In atomic physics, the electron magnetic moment, or more specifically the electron magnetic dipole moment, is the magnetic moment of an electron resulting from its intrinsic properties of spin and electric charge. The value of the electron magnetic moment is −9.2847646917(29)×10⁻²⁴ J⋅T⁻¹. In units of the Bohr magneton (μ_B), it is −1.00115965218059(13) μ_B, a value that was measured with a relative accuracy of 1.3×10⁻¹³.

In physics, the gauge covariant derivative is a means of expressing how fields vary from place to place, in a way that respects how the coordinate systems used to describe a physical phenomenon can themselves change from place to place. The gauge covariant derivative is used in many areas of physics, including quantum field theory and fluid dynamics and in a very special way general relativity.

In mathematics and economics, transportation theory or transport theory is a name given to the study of optimal transportation and allocation of resources. The problem was formalized by the French mathematician Gaspard Monge in 1781.

In quantum computing, quantum finite automata (QFA) or quantum state machines are a quantum analog of probabilistic automata or a Markov decision process. They provide a mathematical abstraction of real-world quantum computers. Several types of automata may be defined, including measure-once and measure-many automata. Quantum finite automata can also be understood as the quantization of subshifts of finite type, or as a quantization of Markov chains. QFAs are, in turn, special cases of geometric finite automata or topological finite automata.

In statistics, the inverse Wishart distribution, also called the inverted Wishart distribution, is a probability distribution defined on real-valued positive-definite matrices. In Bayesian statistics it is used as the conjugate prior for the covariance matrix of a multivariate normal distribution.

In quantum mechanics, the Pauli equation or Schrödinger–Pauli equation is the formulation of the Schrödinger equation for spin-1/2 particles, which takes into account the interaction of the particle's spin with an external electromagnetic field. It is the non-relativistic limit of the Dirac equation and can be used where particles are moving at speeds much less than the speed of light, so that relativistic effects can be neglected. It was formulated by Wolfgang Pauli in 1927. In its linearized form it is known as Lévy-Leblond equation.

In mathematical physics, spacetime algebra (STA) is the application of Clifford algebra Cl_1,3(R), or equivalently the geometric algebra G(M⁴) to physics. Spacetime algebra provides a "unified, coordinate-free formulation for all of relativistic physics, including the Dirac equation, Maxwell equation and General Relativity" and "reduces the mathematical divide between classical, quantum and relativistic physics."

In mathematics — specifically, in stochastic analysis — the infinitesimal generator of a Feller process is a Fourier multiplier operator that encodes a great deal of information about the process.

In computer science, more specifically in automata and formal language theory, nested words are a concept proposed by Alur and Madhusudan as a joint generalization of words, as traditionally used for modelling linearly ordered structures, and of ordered unranked trees, as traditionally used for modelling hierarchical structures. Finite-state acceptors for nested words, so-called nested word automata, then give a more expressive generalization of finite automata on words. The linear encodings of languages accepted by finite nested word automata gives the class of visibly pushdown languages. The latter language class lies properly between the regular languages and the deterministic context-free languages. Since their introduction in 2004, these concepts have triggered much research in that area.

In mathematical physics, the Belinfante–Rosenfeld tensor is a modification of the stress–energy tensor that is constructed from the canonical stress–energy tensor and the spin current so as to be symmetric yet still conserved.

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. Further, clocks can be reset. Timed automata are a sub-class of a type hybrid automata.

Lagrangian field theory is a formalism in classical field theory. It is the field-theoretic analogue of Lagrangian mechanics. Lagrangian mechanics is used to analyze the motion of a system of discrete particles each with a finite number of degrees of freedom. Lagrangian field theory applies to continua and fields, which have an infinite number of degrees of freedom.

In model checking, a subfield of computer science, a clock is a mathematical object used to model time. More precisely, a clock measures how much time passed since a particular event occurs, in this sense, a clock is more precisely an abstraction of a stopwatch. In a model of some particular program, the value of the clock may either be the time since the program was started, or the time since a particular event occurred in the program. Those clocks are used in the definition of timed automaton, signal automaton, timed propositional temporal logic and clock temporal logic. They are also used in programs such as UPPAAL which implement timed automata.

In model checking, a field of computer science, timed propositional temporal logic (TPTL) is an extension of propositional linear temporal logic (LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event p is eventually followed by an event q, TPTL furthermore allows to give a time limit for q to occur.

In automata theory, a field of computer science, a signal automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a signal 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. Further, clocks can be reset.

In model checking, a field of computer science, a region is a convex polytope in $for some dimension, and more precisely a zone, satisfying some minimality property. The regions partition .$

In theoretical physics, more specifically in quantum field theory and supersymmetry, supersymmetric Yang–Mills, also known as super Yang–Mills and abbreviated to SYM, is a supersymmetric generalization of Yang–Mills theory, which is a gauge theory that plays an important part in the mathematical formulation of forces in particle physics. It is a special case of 4D N = 1 global supersymmetry.

References

1 2 3 4 Lasota, SƗawomir; Walukiewicz, Igor (2008). "Alternating Timed Automata". ACM Transactions on Computational Logic. 9 (2): 1–26. arXiv: 1208.5909 . doi:10.1145/1342991.1342994. S2CID 12319.
1 2 Shankar, Priti; D'souza, Deepak (2012-05-24). Modern Applications Of Automata Theory. World Scientific. ISBN 978-981-4468-32-9.
↑ Chandra, Ashok K.; Kozen, Dexter C.; Stockmeyer, Larry J. (January 1981). "Alternation". Journal of the ACM. 28 (1): 114–133. doi:10.1145/322234.322243. ISSN 0004-5411.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[Alternating_timed_automata-1] 1 2 3 4 Lasota, SƗawomir; Walukiewicz, Igor (2008). "Alternating Timed Automata". ACM Transactions on Computational Logic. 9 (2): 1–26. arXiv: 1208.5909 . doi:10.1145/1342991.1342994. S2CID 12319.

[:0-2] 1 2 Shankar, Priti; D'souza, Deepak (2012-05-24). Modern Applications Of Automata Theory. World Scientific. ISBN 978-981-4468-32-9.

[3] Chandra, Ashok K.; Kozen, Dexter C.; Stockmeyer, Larry J. (January 1981). "Alternation". Journal of the ACM. 28 (1): 114–133. doi:10.1145/322234.322243. ISSN 0004-5411.

[1]

[2]

[3]