figure 1. several refinements of a model (a) of the working mathematician according to erdős: after insertion of a coin into the coffee
dispenser, coffee can be collected, and the scientist can go back to work. in the timed-automaton model (b), precisely five time units pass
between coin insertion and coffee collection, and the time which passes between coin insertion and going back to work is less than 10
time units. in the priced timed automaton (c), cost rates (modeling, for example, energy consumption) are associated with the three states.
in the timed game (d), uncertainty as to precisely when coffee is delivered is modeled as an uncontrolled edge.
location problems have manifested
themselves under different names in
application domains such as manufacturing, transport, communication
networks, embedded systems, and
digital circuits, and have been treated
using theories and methods in several
disciplines. Most of these applications
involve distributed, reactive systems
of considerable complexity, and with
a number of real-time constraints in
the sense that correctness not only depends on the logical ordering of events
of the systems, but also on the relative
timing between these.
State-based models have been
the basis of a wide range of successful computer-supported verification
methodologies allowing the efficient
prediction of functional properties,
for example, absence of deadlock or
memory overflow. However, many of
the models used in this methodology
are purely discrete and their treatment
of time is purely qualitative, that is, behaviors are just sequences of events appearing one after the other but without
any quantitative timing information
about the duration of actions and the
time between events. Timed automata
allow such timing constraints to be expressed, while being amenable to computer-aided analysis methods such as
simulation, verification, optimization,
and controller synthesis.
Performance: In all of the above
applications, an explicit constraint
on timing is only one of a number of
quantitative aspects of importance.
Within embedded systems additional key quantities include energy and
memory consumption, in communication networks required bandwidth
is a key quantity, and within the factory and supply chain applications need
for storage and overall cost for a given
production are crucial quantities. The
extended notion of priced or weighted
timed automata has been put forward
as a formalism allowing for such additional and time-dependent quantities
to be modeled, without hampering efficient analysis and even permitting
optimization.
Uncertainty: Classical models for
scheduling in manufacturing, such
as job-shop problems, are somewhat
detached from industrial practice and
reality. They assume that the duration
of every step as well as the arrival times
are fixed and known with certainty; in
practice however, it is rarely the case
that a schedule is executed as planned.
For solving problems related to
expected time and performance properties, stochastic process models have been
very successful. When aiming at
guaranteed time and performance properties under uncertainty, so-called timed
games may be used instead. They provide
efficient offline algorithms for synthesizing reactive schedulers with performance guarantees. Such algorithms
can plan for the best or worst case, but
the scheduling strategies they produce
are adaptive and can take advantage,
for example, of the fact that a task has
terminated before it was expected to.
In this article we present the formalism of timed automata and its priced
and game extension as a unifying
mathematical framework for the modeling, analysis, optimization, and synthesis of real-time related phenomena.
Figure 1 shows some simple examples
of these formalisms; later we provide
more elaborate and realistic examples
and case studies.
timed automata
A model for time. Timed automata5
are a powerful model for representing and reasoning about systems
where the notion of time is essential. They are an extension of classical finite-state automata with real-
valued variables called clocks. These
clocks all increase at the same rate,
and their values can be used to restrict availability of transitions and
how long one can stay in a location
(or state). Also, clocks can be reset
to zero when a transition is taken. To
this end, each transition has associated with it a guard (which must be
satisfied for the transition to be enabled) and a set of clocks to be reset,
and each location carries an invariant
that must be continuously satisfied
when the system is in the location.
Below we show an example of a timed
automaton with two clocks x and y,
and label set {a, b, c, d, e}. Note that
no time can elapse in location 1 due
to the invariant ( y = 0); locations with
this property are called urgent.
2;
=2
( =0)
≤2 :=0
;0 ;
1
3;
=2
Guards and invariants are given
as comparisons x ≤ a or x<a, or the
reverse relations, of a clock value with
an integer constant, or as conjunctions
of these. Sometimes also so-called
diagonal constraints x − y ≤ a (or < or
other) are allowed, but other extensions quickly lead to undecidability
issues, see below.
A configuration of the system is
made of a location and a clock valuation (in our case, values for both clocks
x and y). A possible execution in our
example is:
where the first component of a configuration is the location and the second
