TY - JOUR AU - Behrmann, Gerd AU - Fehnker, Ansgar AU - Hune, Thomas S. AU - Larsen, Kim G. AU - Pettersson, Paul AU - Romijn, Judi PY - 2001/01/04 Y2 - 2024/03/29 TI - Efficient Guiding Towards Cost-Optimality in UPPAAL JF - BRICS Report Series JA - BRICS VL - 8 IS - 4 SE - Articles DO - 10.7146/brics.v8i4.20458 UR - https://tidsskrift.dk/brics/article/view/20458 SP - AB - <p>In this paper we present an algorithm for efficiently computing<br /> the minimum cost of reaching a goal state in the model of Uniformly<br />Priced Timed Automata (UPTA). This model can be seen as a submodel<br />of the recently suggested model of linearly priced timed automata, which<br />extends timed automata with prices on both locations and transitions.<br />The presented algorithm is based on a symbolic semantics of UTPA, and<br />an efficient representation and operations based on difference bound <br />matrices. In analogy with Dijkstra's shortest path algorithm, we show that<br />the search order of the algorithm can be chosen such that the number of<br />symbolic states explored by the algorithm is optimal, in the sense that<br />the number of explored states can not be reduced by any other search<br />order based on the cost of states. We also present a number of techniques<br />inspired by branch-and-bound algorithms which can be used for limiting<br />the search space and for quickly finding near-optimal solutions.<br />The algorithm has been implemented in the verification tool Uppaal.<br />When applied on a number of experiments the presented techniques <br />reduced the explored state-space with up to 90%.</p> ER -