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 proceedingChapterAcademicpeer-review

91 Citations (Scopus)
22 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 languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings
EditorsGérard Berry, Hubert Comon, Alain Finkel
Place of PublicationHeidelberg
PublisherSpringer
Pages493-505
Number of pages13
Volume2102
ISBN (Electronic)978-3-540-44585-2
ISBN (Print)978-3-540-42345-4
DOIs
Publication statusPublished - 2001
Event13th International Conference on Computer Aided Verification, CAV 2001 - Paris, France
Duration: 18 Jul 200122 Jul 2001
Conference number: 13

Publication series

NameLecture Notes in Computer Science
Number2102
ISSN (Print)0302-9743

Workshop

Workshop13th International Conference on Computer Aided Verification, CAV 2001
Abbreviated titleCAV
CountryFrance
CityParis
Period18/07/0122/07/01

Fingerprint

Timed Automata
Reachability
Costs
Facet
Linearly
Entire
Computing
Experiment
Model

Keywords

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

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 proceedingChapterAcademicpeer-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