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

  • 78 Citations

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
StatePublished - 2001

Publication series

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

Fingerprint

Costs
Machinery
Experiments

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. DOI: 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. 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-reviewChapter

@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",
isbn = "978-3-540-42345-4",
volume = "2102",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "2102",
pages = "493--505",
editor = "Gé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. DOI: 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: Scientific - peer-reviewChapter

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 -

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). Available from, DOI: 10.1007/3-540-44585-4_47