文章基本信息

标题：Minimum-Cost Reachability for Priced Timed Automata
本地全文：下载
作者：Gerd Behrmann ; Ansgar Fehnker ; Thomas S. Hune 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2001
卷号：8
期号：3
出版社：Aarhus University
摘要：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.