A Faster Algorithm for Solving One-Clock Priced Timed Games

TL;DR

This paper introduces a new algorithm for one-clock priced timed games that significantly improves the computational complexity from exponential to subexponential time, leveraging geometric and decision process techniques.

Contribution

We present a novel algorithm combining sweep-line and strategy iteration methods, reducing the time complexity for solving one-clock priced timed games.

Findings

Achieved a time complexity of m 12^n n^{O(1)}

Improved previous bounds from 2^{O(n^2+m)}

Enhanced analysis of existing algorithms

Abstract

One-clock priced timed games is a class of two-player, zero-sum, continuous-time games that was defined and thoroughly studied in previous works. We show that one-clock priced timed games can be solved in time m 12^n n^(O(1)), where n is the number of states and m is the number of actions. The best previously known time bound for solving one-clock priced timed games was 2^(O(n^2+m)), due to Rutkowski. For our improvement, we introduce and study a new algorithm for solving one-clock priced timed games, based on the sweep-line technique from computational geometry and the strategy iteration paradigm from the algorithmic theory of Markov decision processes. As a corollary, we also improve the analysis of previous algorithms due to Bouyer, Cassez, Fleury, and Larsen; and Alur, Bernadsky, and Madhusudan.