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.
Timed automata can be used to model and analyse the timing behavior of computer systems, e.g., real-time systems or networks.
Methods for checking both safety and liveness properties have been developed and intensively studied over the last 20 years.
It has been shown that the state reachability problem for timed automata is decidable,[1] which makes this an interesting sub-class of hybrid automata.
Extensions have been extensively studied, among them stopwatches, real-time tasks, cost functions, and timed games.
There exists a variety of tools to input and analyse timed automata and extensions, including the model checkers UPPAAL, Kronos, and the schedulability analyser TIMES.
Before formally defining what a timed automaton is, some examples are given.
A timed automaton recognizing this language, pictured nearby, uses a single clock
This clock counts the time since the start of the run if no
The timed automaton recognizing this language, pictured nearby, recalls whether or not there was an
If it is not the case, it accepts the run, otherwise it rejects it.
cannot be emitted if the clock is at least equal to one, and thus the run fails.
Note that the word state is thus ambiguous, since, depending on the author, it may mean either a pair or an element of
For the sake of the clarity, this article will use the term location for element of
In a finite automaton, at some point of the execution, the state is entirely described by the number of letter read and by a finite number of possible values, which are actually called "states".
That means that, given a state and a suffix of the word to read, the remaining of the run is totally determined.
However, as it is explained in the section "run" below, in order to resume clocks are used to determine which transitions can be taken.
Thus, in order to know the state of the automaton, you must both know in which location you are, and the clock valuation.
an increasing sequence of non-negative number, and a timed automaton
satisfying the following constraint: The notion of accepting run is defined as in finite automata for finite words and as in Büchi automata for infinite words.
It means that the set of start locations is a singleton, and that, given a state
However, in the case of timed automaton the formal definition is slightly more complex.
Formally, a timed automaton is deterministic if: The class of languages recognized by non-deterministic timed automata is: The computational complexity of some problems related to timed automata are now given.
The emptiness problem for timed automata can be solved by constructing a region automaton and checking whether it accepts the empty language.
[1]: 207 The universality problem of non-deterministic timed automaton is undecidable, and more precisely Π11.
However, when the automaton contains a single clock, the property is decidable; however, it is not primitive recursive.
[3] This problem consists of deciding whether every word is accepted by a timed automaton.
