Paper Info
Title
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. 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%.
Year
Venue
Keywords
2001
TACAS
shortest path algorithm,branch-and-bound algorithm,symbolic state,search space,goal state,symbolic semantics,explored state,efficient guiding towards cost-optimality,explored state-space,search order,efficient representation
Field
DocType
ISBN
Knowledge representation and reasoning,Shortest path problem,Computer science,Matrix (mathematics),Automaton,Symbolic computation,Algorithm,Theoretical computer science,Real-time operating system,Formal verification,Dijkstra's algorithm
Conference
3-540-41865-2
Citations 
PageRank 
References 
64
3.93
10
Authors
6
Name
Order
Citations
PageRank
Gerd Behrmann1164881.69
Ansgar Fehnker273648.68
Thomas Hune323016.61
Kim G. Larsen43922254.03
Paul Pettersson52636174.89
Judi Romijn620716.19