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). The central contribution of this paper is a priced extension of so-called zones. This, together with a notion of facets of a zone, allows the entire machinery for symbolic reachability for timed automata 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.
|Title of host publication||Computer aided verification : proceedings 13th international conference, CAV 2001, Paris, july 18-22, 2001|
|Editors||G. Berry, H. Comon, A. Finkel|
|Publication status||Published - 2001|
|Name||Lecture Notes in Computer Science|