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. |
Year | Venue | Keywords |
---|---|---|
2001 | CAV | efficient cost-optimal reachability,symbolic reachability,entire machinery,optimal cost,priced timed automata,so-called zone,goal state,central contribution,cost-optimizing extension |
Field | DocType | Volume |
Transition system,Computer science,Automaton,Algorithm,Theoretical computer science,Reachability,Real-time operating system,Timed automaton,Symbolic execution,Hybrid system,Formal verification | Conference | 2102 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-42345-1 | 53 |
PageRank | References | Authors |
3.55 | 20 | 7 |
Name | Order | Citations | PageRank |
---|---|---|---|
Kim Guldstrand Larsen | 1 | 4434 | 346.88 |
Gerd Behrmann | 2 | 1648 | 81.69 |
Ed Brinksma | 3 | 1676 | 210.11 |
Ansgar Fehnker | 4 | 736 | 48.68 |
Thomas Hune | 5 | 230 | 16.61 |
Paul Pettersson | 6 | 2636 | 174.89 |
Judi Romijn | 7 | 207 | 16.19 |