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

TL;DR

This paper introduces a new theoretical framework and an improved algorithm for two-player reachability-price games on single-clock timed automata, reducing the computational complexity from 3EXPTIME to EXPTIME.

Contribution

It develops a comprehensive theory of cost functions and presents an EXPTIME algorithm that improves upon the previous 3EXPTIME upper bound.

Findings

Established a theory of cost functions for analysis.

Developed an EXPTIME algorithm for computing optimal reachability prices.

Reduced the complexity bound from 3EXPTIME to EXPTIME.

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.