Efficient Guiding Towards Cost-Optimality in UPPAAL

Abstract

In this paper we present an algorithm for efficiently computing
the minimum cost of reaching a goal state in the model of Uniformly
Priced Timed Automata (UPTA). This model can be seen as a submodel
of the recently suggested model of linearly priced timed automata, which
extends timed automata with prices on both locations and transitions.
The presented algorithm is based on a symbolic semantics of UTPA, and
an efficient representation and operations based on difference bound
matrices. In analogy with Dijkstra's shortest path algorithm, we show that
the search order of the algorithm can be chosen such that the number of
symbolic states explored by the algorithm is optimal, in the sense that
the number of explored states can not be reduced by any other search
order based on the cost of states. We also present a number of techniques
inspired by branch-and-bound algorithms which can be used for limiting
the search space and for quickly finding near-optimal solutions.
The algorithm has been implemented in the verification tool Uppaal.
When applied on a number of experiments the presented techniques
reduced the explored state-space with up to 90%.