In
automata theory, a timed automaton is a
finite automaton
A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...
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 In automata theory, a hybrid automaton (plural: ''hybrid automata'' or ''hybrid automatons'') is a mathematical model for precisely describing hybrid systems, for instance systems in which digital computational processes interact with analog physica ...
.
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
Reachability is a fundamental problem that appears in several different contexts: finite- and infinite-state variable, state concurrent systems, computational models like cellular automata and Petri nets, program analysis, Discrete system, discret ...
for timed automata is decidable,
[Rajeev Alur, David L. Dill. 199]
A Theory of Timed Automata
In Theoretical Computer Science, vol. 126, 183–235, pp. 194–1955 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
of
timed-words
over the unary alphabet
such that there is an
during the first time unit, and there is less than one time unit between two successive
. The timed automaton recognizing this language, pictured nearby, use a single
clock
A clock or a timepiece is a device used to measure and indicate time. The clock is one of the oldest human inventions, meeting the need to measure intervals of time shorter than the natural units such as the day, the lunar month and ...
, which should never be equal to one. This clock counts the time since the start of the run if no
were emitted, or from the last
emitted otherwise. This means that each time an
is emitted, this clock is reset to zero.
Consider the language
of
timed-words
over the binary alphabet
such that each
is followed by a
in the next time unit. The timed automaton recognizing this language, pictured nearby, recalls whether there was a
which was not followed by a
or not. If it is not the case, it accepts the run, otherwise it rejects it. Furthermore, when there is such a
, it has a clock
which recall the time elapsed since the first such
was emitted. In this case, a
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
that consists of the following components:
*
is a finite set called the alphabet or actions of
.
*
is a
finite set. The elements of
are called the locations or states' of
.
*
is the set of start locations.
*
is a finite set called the ''
clocks of
.
*
is the set of accepting locations.
*
is a set of edges, called transitions of
, where
**
is the set of
clock constraints involving clocks from
, and
**
is the
powerset of
.
An edge
from
is a transition from locations
to
with action
, guard
and clock resets
.
Extended state
A pair with a location
and a
clock valuation 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
. For the sake of the clarity, this article will use the term location for element of
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 In model checking, a subfield of computer science, a timed word is an extension of the notion of words, in a formal language, in which each letter is associated with a positive time tag. The sequence of time tag must be non-decreasing, which intui ...
with
,
an increasing sequence of non-negative number, and a timed-automaton
as above, a ''run'' is a sequence of the form
satisfying the following constraint:
* (initialization)
* (consecution), for all
, there exists an edge in
of the form
such that:
** we assume that
time units passed, and at this time, the guard is satisfied. I.e.
satisfies
,
** the new clock valuation
corresponds to
, in which
time units passed and in which the clocks of
where reset. Formally,