Timed automata are a well-established model for real-time systems.
One of the most important they enjoy is that reachability and temporal
logic properties are decidable. This has given rise to multiple works,
both on the theoretical aspects and more practical and algorithmic
aspects. In particular a number of mature tools for model-checking
for model has emerged (e.g. UPPAAL and Kronos) with a growing number
of successful applications to validation of industrial case-studies
(see the UPPAAL homepage for more information).
Whereas UPPAAL allows for the validation of GIVEN scheduling
strategies and control programs a substantial amount of recent
research is working towards automatic synthesis of (optimal)
scheduling strategies and control programs which are now available in
two new branches of UPPAAL: UPPAAL Cora and UPPAAL Tiga.
UPPAAL Cora uses a priced (or weighted) timed automata as the
underlying modeling formalism. Priced timed automata extend classical
timed automata with cost information on location (and edges) giving
the price per time unit for staying in that location. In this way
every run of a priced automaton has a global cost. A number of
natural optimization problems has dealt with in both in terms of basic
computability but also in terms of datastructures and algoritms for
efficient implementation in practice. By now UPPAAL Cora has been used
in a number case studies including a number of classical (benchmark)
scheduling problems as well as several industrial planning and
scheduling problems.
UPPAAL Tiga deals with OPEN systems, i.e. systems interacting with an
environment, with the purpose of synthesizing a control so that the
system behaves correct no matter what the environment does. Formally,
UPPAAL Tiga uses timed GAME automata to model such open systems as a
(real-time) game between the "controller" and the "environment". More
concretely edges of a timed game automaton are either "controllable"
(thus describing possible moves of the controller) or "uncontrollable"
(thus describing possible moves of the environment). Though timed
games for long have been known to be decidable there has until now
been a lack of efficient algorithm. UPPAAL Tiga offers the first
efficient on-the-fly algorithm for synthesizing winning strategies for
timed game automata with respect to reachability and safety
properties. Current applications include synthesis of time-optimal
control for the well-known Production Cell case-study and off-line
synthesis of test-suites from NON-DETERMINISTIC timed automata models
with guaranteed model coverage.
