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

Michal Rutkowski
(Department of Computer Science, The University of Warwick)

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 Mieke Massink and Gethin Norman: Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), Saarbrücken, Germany, April 1-3, 2011, Electronic Proceedings in Theoretical Computer Science 57, pp. 31–46.
Published: 4th July 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: