Guiding and CostOptimality in UPPAAL
Paul Pettersson
Information Technology, Uppsala University
Abstract
In this talk, I present recent work on modifying the UPPAAL
modelchecking algorithm for 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 branchandbound algorithms which can be used for limiting the
search space and for quickly finding nearoptimal solutions.
The algorithm has been implemented in the verification tool UPPAAL. When applied
on a number of experiments the presented techniques reduced the explored
statespace with up to 90%.
KEYWORDS: Timed Automata, Optimisation, Verification, Data Structures,
Algorithms.
Place: Information technology, Uppsala University
Room: 1113
Time: 15.1516.00 (+ discussions)
Room 1113 is in Building 1, Floor 1, room 13
(in the southern part of the building).
Help on how to find ASTEC Seminars.
There will be an extended period for discussions after the seminar.
Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 16.00.
Everyone is welcome !
Updated 04Apr2001 16:07 by Roland Grönroos
email: info at astec.uu.se
Location: http://www.astec.uu.se/Seminars/01/0410.shtml
