Two-Player Reachability-Price Games on Single-Clock Timed Automata

Abstract

We study two player reachability-price games on single-clock timed automata. The problem is as follows: given a state of the automaton, determine whether the first player can guarantee reaching one of the designated goal locations. If a goal location can be reached then we also want to compute the optimum price of doing so. Our contribution is twofold. First, we develop a theory of cost functions, which provide a comprehensive methodology for the analysis of this problem. This theory allows us to establish our second contribution, an EXPTIME algorithm for computing the optimum reachability price, which improves the existing 3EXPTIME upper bound.

In Proceedings QAPL 2011, arXiv:1107.0746

References in corpus (1)

• Average-Time Games on Timed Automata

Cited by in corpus (8)

• Simple Priced Timed Games Are Not That Simple
• Optimal controller synthesis for timed systems
• Adding Negative Prices to Priced Timed Games
• One-Clock Priced Timed Games with Negative Weights
• A Faster Algorithm for Solving One-Clock Priced Timed Games
• Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond
• Revisiting Robustness in Priced Timed Games
• Optimal Reachability in Divergent Weighted Timed Games