Communications - September 2011

emerges related to the appropriate management of resources: “Is it possible to maintain the level of resources within fixed bounds?” Such resource-bound problems are highly relevant to the analysis of several embedded systems, for example, it is natural to plan the usage of a device with rechargeable batteries so that one never runs out of energy, nor exceeds the maximum capacity for energy storage. Figure 5 shows a priced timed automaton together with some resource management problems.

Few results have been obtained on this problem so far: only the case of one-clock priced timed automata has been investigated. 15 This restriction has two important consequences: cycle detection can be done statically, as each resetting transition leads to a configuration with clock value 0, and the region automaton can be coarsened so that the partition consists of intervals with end-points given by the constants in the automaton’s guards. As a consequence, there are only polynomially many regions.

Under the additional assumption that the cost cannot be updated during transitions (hence cost evolves only in locations), it can be shown15 that for finding runs that satisfy a global lower-bound constraint, with or without soft upper bound, one can restrict oneself to look for runs with integral delays. Hence, the corner-point abstraction can be used for this, and the problems are solvable in polynomial time.

For priced timed automata with
more than one clock, no results are
known, but even for one-clock autom-
ata with cost updates during transi-
tions, there are some difficulties that
mean abstractions like the above are
insufficient. As an example, consider
the following priced timed automaton:

= 1 :=0

0

+ 2

;

1

+ 2

;

2

+ 4 − 3

;

Assuming that we start with initial cost 0, this automaton has exactly one feasible execution in which the cost level remains non-negative: after spending one time unit in location 0, we alternately spend half a time unit in 1 and half a time unit in 2. Any other execution eventually violates the lower bound. Hence in this case, runs satisfying the lower bound cannot be found using the corner-point abstraction.

Priced timed Games a model for uncertainties. The systems we have considered so far are closed in the sense that we have a complete description of the system. This is not sufficient to model embedded systems where interaction with the environment is crucial, or systems with some imprecision. These can be modeled using (two-player) timed games, 8 in which some actions are triggered by the environment (we can think of signals received by sensors, or of unexpected events). The aim is to control, or guide, the system so that it will be safe or correct regardless of the way the environment interferes. An example of a timed game is depicted below:

2;

= 2

≤ 2 :=0

0;

1

( =0)

;

3;

= 2

Dashed edges belong to the environment (they are uncontrollable): when they are fireable, the system cannot prevent (nor force) them to be fired. Here, the system cannot decide whether it goes through 2 or through 3.

For simple correctness criteria, for example, reachability or safety, the set of winning states (that is, states from which the system can be controlled under the safety constraint) and also winning strategies (that is, policies for how to control the system) can be computed using the region abstraction. 8 Also computability of time-optimal strategies, 7 as well as strategies under partial observability, has been demonstrated. For the latter, decisions are based on discrete observations giving only partial information of the system state, depending on the availability and precision of sensors. 19 For efficient algorithms, a zone-based approach for solving timed games with reachability and safety objectives has been developed, 18, 38 and tool support is available in Uppaal-Tiga.

task graph scheduling: timing uncertainty. Returning to our running task graph scheduling example, we can use the formalism of timed games to model uncertainty in precisely how much time a certain computation on a given processor takes. Previously, we modeled computation times by precise numbers, whereas we now can make the model more realistic by only providing interval bounds within which computation times are prescribed to lie. The timed game models below provide versions of the processors P1 and P2 from Figure 3 in which computation times are prescribed to lie in the intervals [ 1, 2] for addition and [ 1, 3]

figure 5. The resource management problem asks whether it is possible to maintain the cost level within fixed bounds. there can be a lower bound only (a), a lower and an upper bound (b, c), or a lower bound and a soft upper bound above which cost level cannot increase. figures (a), (b), and (d) represent solutions to the respective problems for the priced timed automaton depicted on the left: there is an infinite run that satisfies the global constraint. in case (a) for instance, we have depicted a possible schedule for the first cycle, and this run can be repeated because at the start of the second cycle, the cost level is larger than at the start of the first cycle. in figure (c), the proposed schedule violates the lower bound, and it can be shown that there exists no infinite run which maintains cost level within the specified bounds.