Efficient Guiding Towards Cost-Optimality in UPPAAL

Abstract

<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>