As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata

Kim Larsen Gerd Behrmann Ed Brinksma Ansgar Fehnker Thomas Hune Paul Pettersson Judi Romijn

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems