Open AccessMinimum-Cost Reachability for Priced Timed Automata
Author(s) -
Gerd Behrmann,
Ansgar Fehnker,
Thomas Hune,
Kim G. Larsen,
Paul Pettersson,
Judi Romijn,
Frits Vaandrager
Publication year - 2001
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v8i3.20457
Subject(s) - reachability , decidability , automaton , timed automaton , computer science , reachability problem , state (computer science) , model checking , finite state machine , extension (predicate logic) , discrete mathematics , mathematics , algorithm , theoretical computer science , programming language
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. Keywords: Timed Automata, Verification, Data Structures, Algorithms, Optimization.