Abstract
In this paper we present an algorithm for efficiently computing optimal cost of reaching a goal state in the model of Linearly Priced Timed Automata (LPTA). The central contribution of this paper is a priced extension of so-called zones. This, together with a notion of facets of a zone, allows the entire machinery for symbolic reachability for timed automata in terms of zones to be lifted to cost-optimal reachability using priced zones. We report on experiments with a cost-optimizing extension of UPPAAL on a number of examples.
Original language | English |
---|---|
Title of host publication | Computer Aided Verification |
Subtitle of host publication | 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings |
Editors | Gérard Berry, Hubert Comon, Alain Finkel |
Place of Publication | Heidelberg |
Publisher | Springer |
Pages | 493-505 |
Number of pages | 13 |
Volume | 2102 |
ISBN (Electronic) | 978-3-540-44585-2 |
ISBN (Print) | 978-3-540-42345-4 |
DOIs | |
Publication status | Published - 2001 |
Event | 13th International Conference on Computer Aided Verification, CAV 2001 - Paris, France Duration: 18 Jul 2001 → 22 Jul 2001 Conference number: 13 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Number | 2102 |
ISSN (Print) | 0302-9743 |
Workshop
Workshop | 13th International Conference on Computer Aided Verification, CAV 2001 |
---|---|
Abbreviated title | CAV |
Country/Territory | France |
City | Paris |
Period | 18/07/01 → 22/07/01 |
Keywords
- METIS-205778
- EWI-6457
- FMT-MC: MODEL CHECKING
- FMT-TOOLS
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
- IR-63285
- FMT-SEMANTICS