figure 4. The corner-point abstraction refines the region abstraction by also keeping track of the corner point close to which an execution runs. this is needed to measure costs: for instance, if we are in location 1 and in the red region where 0 < y < x < 1, the price of delaying depends on the value of the clocks. from (a), where both x and y are arbitrarily close to 0, we can let almost one time-unit elapse and reach (b). the resulting cost is arbitrarily close to + 3. o n the other hand, from (c), where x and y are arbitrarily close to 1 and 0, respectively, letting time elapse takes us to the subsequent region, so that the cost is arbitrarily close to 0. (notice that for readability, some resetting transitions have been omitted.)

 

example, the two-dimensional region depicted below is refined into three region-corner pairs; the meaning of a region-corner pair is that the current clock valuation is arbitrarily close to the distinguished corner:

 

(a)

(b)

(c)

 

Similar to the refinement of regions, the transitions in the region automaton have to be refined to keep track of the corners. In the example above, there is a (delay) transition from region-corner pair (a) to (b), whereas (c) cannot be reached neither from (a) nor from (b). Figure 4 illustrates the corner-point abstraction of an example priced timed automaton. This graph has two types of delay edges: either within a region, from one corner to another one, or from a corner of a region to the corresponding corner in the subsequent region. The first case corresponds to a delay of “almost” one time unit, while the second case corresponds to a delay of “almost” zero time units. In addition, there are edges representing transitions of the timed automaton (which reset clock x in our example of Figure 4). In that case as well, there is a natural mapping between corners.

The edges of the corner-point ab-
straction are labeled with discrete cost
information: if the cost rate in the cur-
rent location is + 3, all one time-unit
edges have label + 3, and all zero time-
unit edges get label 0. Edges coming
from discrete transitions are labeled
with the cost of the transition (+ 5 in
the example).

steps is modeled as cost in the priced timed automaton model, and optimal reachability techniques can be used for finding an energy-optimal schedule.

For the task graph scheduling instance of Figure 3, energy consumption of the two processors is reflected in the respective timed automata by suitable cost-rates in the locations corresponding to the processor being idle or in use. The processors can then be represented by the following two priced timed automata:

1:

+

( ≤ 2)

+ 90

×

( ≤ 3)

+ 90

2:

+

( ≤ 5)

+ 30

idle

+ 10

:=0 add1

= 2 done1

idle

+ 20

:=0 add2

= 5 done2

:=0 mult1

= 3 done1

:=0 mult2

= 7 done2

×

( ≤ 7)

+ 30

 

managing the resources. Up to this point we have only employed priced timed automata as a formalism for modeling time-dependent consumption of resources. However, in several situations resources may not just be consumed but also occasionally regained, for example, in autonomous robots with rechargeable batteries, or in tanks which may not only be emptied but also filled. Extending priced timed automata to allow for both positive (regaining) and negative ( consumption) rates provides a natural modeling formalism. 21

However, a new question now