Abstract
| 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 | |
| State | Published - 2001 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Number | 2102 |
| ISSN (Print) | 0302-9743 |
Fingerprint
Keywords
- METIS-205778
- EWI-6457
- FMT-MC: MODEL CHECKING
- FMT-TOOLS
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
- IR-63285
- FMT-SEMANTICS
Cite this
}
As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata. / Larsen, K.G.; Behrmann, Gerd; Brinksma, Ed; Fehnker, Ansgar; Hune, Thomas; Petterson, Paul; Romijn, J.M.T.; Romijn, Judi.
Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings. ed. / Gérard Berry; Hubert Comon; Alain Finkel. Vol. 2102 Heidelberg : Springer, 2001. p. 493-505 (Lecture Notes in Computer Science; No. 2102).Research output: Scientific - peer-review › Chapter
TY - CHAP
T1 - As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata
AU - Larsen,K.G.
AU - Behrmann,Gerd
AU - Brinksma,Ed
AU - Fehnker,Ansgar
AU - Hune,Thomas
AU - Petterson,Paul
AU - Romijn,J.M.T.
AU - Romijn,Judi
N1 - Proceedings of Computer Aided Verification, Paris, Springer-Verlag
PY - 2001
Y1 - 2001
N2 - 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.
AB - 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.
KW - METIS-205778
KW - EWI-6457
KW - FMT-MC: MODEL CHECKING
KW - FMT-TOOLS
KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
KW - IR-63285
KW - FMT-SEMANTICS
U2 - 10.1007/3-540-44585-4_47
DO - 10.1007/3-540-44585-4_47
M3 - Chapter
SN - 978-3-540-42345-4
VL - 2102
T3 - Lecture Notes in Computer Science
SP - 493
EP - 505
BT - Computer Aided Verification
PB - Springer
ER -