This talk will offer a comprehensive review of priced timed automata and
energy games high lightening results obtained and problems that remain open.
Priced (or weighted) timed automata was introduced in 2001, and
have emerged as a useful formalism for formulating a wide range of resource-allocation and optimization
problems with applications in areas such as embedded systems.
The initial optimization problem considered was that of cost-optimal reachability,
shown to be decidable and PSPACE-complete . Later decidability
and PSPACE-completeness of the problem of optimal infinite runs, in terms of
minimal (maximal) cost per time ratio or accumulated discounted cost has been
In 2008 a new class of resource-allocation problems was introduced, namely
that of constructing infinite schedules subject to boundary constraints on the
accumulation of resources, so-called energy games. We review what is know
about decidability and complexity in terms of number of clocks and number of
cost variables for this problem.
We also show how the use of statistical model checking may be used
to efficiently obtain near optimal solutions.