In this paper we present an algorithm for efficiently computing
optimal cost of reaching a goal state in the model of Linearly Priced
Timed Automata (LPTA). In recent papers, this problem have been shown
to be computable using a priced extention of the traditional notion of
regions for timed automata. However, for efficiency it is imperative
that the computation is based on so-called zones (i.e. convex set of
clock valuations) rather than regions. The central contribution of
this paper is a priced extension of zones. This, together with a
notion of facets of a zone, allows the entire machinery for symbolic
reachability in terms of zones to be lifted to cost-optimal
reachability using priced zones. We report on experiments with a
cost-optimizing extension of Uppaal on a number of examples,
including a range of aircraft landing problems.
