Minimum-Cost Reachability for Priced Timed Automata

By G. Behrmann, A. Fehnker, T. Hune, Kim Guldstrand Larsen, Paul Pettersson, J. Romijn, F. Vaandrager. International Conference on Hybrid Systems: Computation and Control, 2001

377 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/349d3da5767f339a4c65cf121f7e5a74be09a3e2

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. George Pappas
2. Alexandre David
3. Kim Guldstrand Larsen
4. Axel Legay
5. Rajeev Alur
6. Hadas Kress-Gazit
7. Jiri Srba
8. Nicolas Loizou

In Computational Theory and Mathematics

1. George Pappas
2. Kim Guldstrand Larsen
3. Rajeev Alur
4. Alexandre David
5. Axel Legay
6. Antoine Girard
7. Hadas Kress-Gazit
8. Paulo Tabuada

In Software

1. Kim Guldstrand Larsen
2. Alexandre David
3. Rajeev Alur
4. Axel Legay
5. George Pappas
6. Jiri Srba
7. Paulo Tabuada

Citations in the corpus

• A Tutorial on Uppaal (2004, positive): “Experiments and improvements include data structures [46], partial order reduction [18], symmetry reduction [31], a distributed version of Uppaal [15, 9], guided and minimal cost reachability [13, 44, 14], work on UML Statecharts [26], acceleration techniques [32], and new data structures and memory”
• Model Checking Real-Time Systems (2018, neutral): “Weighted timed automata [20, 33] is an intermediary model, extending timed automata with hybrid observer variables: these variables cannot appear in the guards of the automaton, but they can be used, for example, for optimization purposes.”
• Uppaal SMC tutorial (2015, methodology): “Thus, the distributions for A1 and A2 have finite support by the intervals [6, 12] and [4, 12], respectively.”
• Optimal Paths in Weighted Timed Automata (2001, background): “We also recall that the single-source optimal-reachability problem was independently de4ned and solved by [5].”