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. Further, clocks can be reset. Timed automata are a sub-class of a type hybrid automata.
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, 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. These tools are becoming more and more mature, but are still all academic research tools.
Example.
Before formally defining what a timed automaton is, some examples are given.
Consider the language formula_1 of timed-words formula_2 over the unary alphabet formula_3 such that there is an formula_4 during the first time unit, and there is less than one time unit between two successive formula_4. The timed automaton recognizing this language, pictured nearby, use a single clock formula_6, which should never be equal to one. This clock counts the time since the start of the run if no formula_4 were emitted, or from the last formula_4 emitted otherwise. It means that each time an formula_4 is emitted, this clock is reset to zero.
Consider the language formula_1 of timed-words formula_2 over the binary alphabet formula_12 such that each formula_4 is followed by a formula_14 in the next time unit. The timed automaton recognizing this language, pictured nearby, recalls whether there was a formula_4 which was not followed by a formula_14 or not. If it is not the case, it accepts the run, otherwise it rejects it. Furthermore, when there is such a formula_4, it has a clock formula_6 which recall the time elapsed since the first such formula_4 was emitted. In this case, a formula_14 can not be emitted if the clock is at least equal to one, and thus the run fails.
Formal definition.
Timed automaton.
Formally, a timed automaton is a tuple formula_21 that consists of the following components:
An edge formula_37 from formula_38 is a transition from locations formula_39 to formula_40 with action formula_41, guard formula_42 and clock resets formula_43.
Extended state.
A pair with a location formula_39 and a clock valuation formula_45 is called either an "extended state" or a "state".
Note that the word state is thus ambiguous, since, depending on the author, it may mean either a pair or an element of formula_24. For the sake of the clarity, this article will use the term location for element of formula_24 and the term extended location for pairs.
Here lies one of the biggest difference between timed-automata and finite automata. 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. Thus, the word "finite" in the name "finite automata". 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.
Run.
Given a timed word formula_48 with formula_49, formula_50 an increasing sequence of non-negative number, and a timed-automaton formula_23 as above, a "run" is a sequence of the form formula_52 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. That is, if formula_2 is finite of length formula_66, then the run is accepting if formula_67. If the word is infinite, then the run is accepting if and only if there exists an infinite number of position formula_68 such that formula_69.
Deterministic timed automaton.
As in the case of finite and Büchi automaton, a timed-automaton may be deterministic or non-deterministic. Intuitively, being deterministic has the same meaning in each of those case. It means that the set of start locations is a singleton, and that, given a state formula_70, and a letter formula_4, there is only one possible state which can be reached from formula_70 by reading formula_4. However, in the case of timed-automaton the formal definition is slightly more complex. Formally, a timed-automaton is deterministic if:
Closure property.
The class of languages recognized by non-deterministic timed automata is:
Problems and their complexity.
The computational complexity of some problems related to timed automata are now given.
The emptiness problem for timed automaton can be solved by constructing a region automaton and checking whether it accepts the empty language. This problem is PSPACE-complete.
The universality problem of non-deterministic timed automaton is undecidable, and more precisely Π. However, when the automaton contains a single clock, the property is decidable, however it is not primitive recursive. This problem consists in deciding whether every words are accepted by a timed-automaton.