As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata

K.G. Larsen; Gerd Behrmann; Ed Brinksma; Ansgar Fehnker; Thomas Hune; Paul Petterson; J.M.T. Romijn; Judi Romijn

doi:10.1007/3-540-44585-4_47

As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata

K.G. Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Petterson, J.M.T. Romijn, Judi Romijn

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

92 Citations (Scopus)

36 Downloads (Pure)

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	https://doi.org/10.1007/3-540-44585-4_47
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	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

Access to Document

10.1007/3-540-44585-4_47

fulltext
open

http://link.springer.de/link/service/series/0558/bibs/2102/21020493.htm

Fingerprint Dive into the research topics of 'As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata'. Together they form a unique fingerprint.

Cite this

Larsen, K. G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Petterson, P., ... Romijn, J. (2001). As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata. In G. Berry, H. Comon, & A. Finkel (Eds.), Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings (Vol. 2102, pp. 493-505). (Lecture Notes in Computer Science; No. 2102). Heidelberg: Springer. https://doi.org/10.1007/3-540-44585-4_47

Larsen, K.G. ; Behrmann, Gerd ; Brinksma, Ed ; Fehnker, Ansgar ; Hune, Thomas ; Petterson, Paul ; Romijn, J.M.T. ; Romijn, Judi. / As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata. Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings. editor / Gérard Berry ; Hubert Comon ; Alain Finkel. Vol. 2102 Heidelberg : Springer, 2001. pp. 493-505 (Lecture Notes in Computer Science; 2102).

@inbook{468bebf28afc4249b6e164093a37a903,

title = "As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata",

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.",

keywords = "METIS-205778, EWI-6457, FMT-MC: MODEL CHECKING, FMT-TOOLS, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, IR-63285, FMT-SEMANTICS",

author = "K.G. Larsen and Gerd Behrmann and Ed Brinksma and Ansgar Fehnker and Thomas Hune and Paul Petterson and J.M.T. Romijn and Judi Romijn",

note = "Proceedings of Computer Aided Verification, Paris, Springer-Verlag",

year = "2001",

doi = "10.1007/3-540-44585-4_47",

language = "English",

isbn = "978-3-540-42345-4",

volume = "2102",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "2102",

pages = "493--505",

editor = "G{\'e}rard Berry and Hubert Comon and Alain Finkel",

booktitle = "Computer Aided Verification",

}

Larsen, KG, Behrmann, G, Brinksma, E , Fehnker, A, Hune, T, Petterson, P, Romijn, JMT & Romijn, J 2001, As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata. in G Berry, H Comon & A Finkel (eds), Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings. vol. 2102, Lecture Notes in Computer Science, no. 2102, Springer, Heidelberg, pp. 493-505, 13th International Conference on Computer Aided Verification, CAV 2001, Paris, France, 18/07/01. https://doi.org/10.1007/3-540-44585-4_47

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: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

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

A2 - Berry, Gérard

A2 - Comon, Hubert

A2 - Finkel, Alain

PB - Springer

CY - Heidelberg

ER -

Larsen KG, Behrmann G, Brinksma E , Fehnker A, Hune T, Petterson P et al. As Cheap as Possible:Efficient Cost-Optimal Reachability for Priced Timed Automata. In Berry G, Comon H, Finkel A, editors, Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings. Vol. 2102. Heidelberg: Springer. 2001. p. 493-505. (Lecture Notes in Computer Science; 2102). https://doi.org/10.1007/3-540-44585-4_47