Event points in one-clock priced timed games

2^nd April 2019, 11:20
Rasmus Ibsen-Jensen

Abstract

Priced timed games is a class of games that can model many verification problems that contain both continues and discrete aspects. In essence, priced games (i.e. the special case without time) is the (obivous) generalization of Dijkstras shortest path problem into a two player turn-based game. Simple priced timed games (which are polynomial time equvivalent to the one clock special case of price timed games) are then the same class of games, except that each player has the option of waiting a real amount of time (with a corresponding cost paid per time unit), but with the requirement that the time is always between 0 and 1.

Strategies for such are a map from states and times into either waiting or successor states (and you cant wait at time 1).
An unusual property of these games is that the run time of the best algorithms are closely aligned with how complicated the strategies and the value functions are (value functions are a map from start time and state to best possible outcome - value functions are continues and piecewise linear). In particular there are a set of points (in time - the set incl 0 and 1), called event points, such that between any pair of adjacent event points the optimal strategy does the same thing in each state (implying that the value functions are linear in the same range). The running time of some of the algoritms are polynomial (down to linear) in the number of event points (times a polynomial in the size of the game).

This is all quite nice, but annoyingly enough, the best bounds on the number of event points is that it is between n^3 and 12^n.

The goal is to improve the lower and/or upper bound.

Note that showing say an exponential lower bound on the number of event points shows a exponential lower bound on the problem (and not just on specific algoritms for it). Conversely a polynomial upper bound implies a polynomial run time of some of the algorithms.