Minimum-Cost Reachability for Priced Timed Automata

Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, Frits W. Vaandrager

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

This paper introduces the model of linearly priced timed automata as an extension of timed automata, with prices on both transitions and locations. For this model we consider the minimum-cost reachability problem: i.e. given a linearly priced timed automaton and a target state, determine the minimum cost of executions from the initial state to the target state. This problem generalizes the minimum-time reachability problem for ordinary timed automata. We prove decidability of this problem by offering an algorithmic solution, which is based on a combination of branch-and-bound techniques and a new notion of priced regions. The latter allows symbolic representation and manipulation of reachable states together with the cost of reaching them.
Original languageEnglish
Title of host publicationHybrid Systems: Computation and Control
Subtitle of host publication4th International Workshop, HSCC 2001 Rome, Italy, March 28–30, 2001 Proceedings
EditorsMaria Domenica Di Benedetto, Alberto L. Sangiovanni-Vincentelli
PublisherSpringer
Pages147-161
Number of pages15
ISBN (Electronic)978-3-540-45351-2
ISBN (Print)978-3-540-41866-5
DOIs
Publication statusPublished - 2001
Externally publishedYes
Event4th International Workshop on Hybrid Systems: Computation and Control 2001 - Rome, Italy
Duration: 28 Mar 200130 Mar 2001
Conference number: 4

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2034

Conference

Conference4th International Workshop on Hybrid Systems: Computation and Control 2001
Abbreviated titleHSCC 2001
Country/TerritoryItaly
CityRome
Period28/03/0130/03/01

Fingerprint

Dive into the research topics of 'Minimum-Cost Reachability for Priced Timed Automata'. Together they form a unique fingerprint.

Cite this