As cheap as possible: efficient cost-optimal reachability for priced timed automata

Kim Larsen; Gerd Behrmann; Ed Brinksma; Ansgar Fehnker; Thomas Hune; Paul Petterson; Judi Romijn

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

As cheap as possible: efficient cost-optimal reachability for priced timed automata

Kim Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Petterson, Judi Romijn

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

121 Citations (Scopus)

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	Berlin
Publisher	Springer, Springer Nature
Pages	493-505
Number of pages	13
ISBN (Print)	9783540423454, 3540423451
DOIs	https://doi.org/10.1007/3-540-44585-4_47
Publication status	Published - 2001
Externally published	Yes
Event	13th International Conference on Computer Aided Verification, CAV 2001 - Palais de la Mutualite, Paris, France Duration: 18 Jul 2001 → 22 Jul 2001

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2102
ISSN (Print)	0302-9743

Conference

Conference	13th International Conference on Computer Aided Verification, CAV 2001
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

Access to Document

10.1007/3-540-44585-4_47

Cite this

Larsen, K., 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 (pp. 493-505). (Lecture Notes in Computer Science; Vol. 2102). Springer, Springer Nature. https://doi.org/10.1007/3-540-44585-4_47

Larsen, Kim ; Behrmann, Gerd ; Brinksma, Ed et al. / 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. Berlin : Springer, Springer Nature, 2001. pp. 493-505 (Lecture Notes in Computer Science).

@inbook{c50eb8e4454c4c1e99643804179aa33e,

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 = "Kim Larsen and Gerd Behrmann and Ed Brinksma and Ansgar Fehnker and Thomas Hune and Paul Petterson and Judi Romijn",

year = "2001",

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

language = "English",

isbn = "9783540423454",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "493--505",

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

booktitle = "Computer Aided Verification",

address = "United States",

note = "13th International Conference on Computer Aided Verification, CAV 2001 ; Conference date: 18-07-2001 Through 22-07-2001",

}

Larsen, K, 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. Lecture Notes in Computer Science, vol. 2102, Springer, Springer Nature, Berlin, 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, Kim; Behrmann, Gerd; Brinksma, Ed et al.
Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18-22, 2001, Proceedings. ed. / Gérard Berry; Hubert Comon; Alain Finkel. Berlin: Springer, Springer Nature, 2001. p. 493-505 (Lecture Notes in Computer Science; Vol. 2102).

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

TY - CHAP

T1 - As cheap as possible

T2 - 13th International Conference on Computer Aided Verification, CAV 2001

AU - Larsen, Kim

AU - Behrmann, Gerd

AU - Brinksma, Ed

AU - Fehnker, Ansgar

AU - Hune, Thomas

AU - Petterson, Paul

AU - Romijn, Judi

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

UR - https://www.scopus.com/pages/publications/0008287887

U2 - 10.1007/3-540-44585-4_47

DO - 10.1007/3-540-44585-4_47

M3 - Chapter

SN - 9783540423454

SN - 3540423451

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, Springer Nature

CY - Berlin

Y2 - 18 July 2001 through 22 July 2001

ER -

Larsen K, 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. Berlin: Springer, Springer Nature. 2001. p. 493-505. (Lecture Notes in Computer Science). doi: 10.1007/3-540-44585-4_47

As cheap as possible: efficient cost-optimal reachability for priced timed automata

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this