## Trading Infinite Memory for Uniform Randomness in Timed Games

*Krishnendu Chatterjee,
Thomas A. Henzinger,
and Vinayak Prabhu*

We consider concurrent two-player timed automaton games with
omega-regular objectives specified as parity conditions. These games
offer an appropriate model for the synthesis of real-time controllers.
Earlier works on timed games focused on pure strategies for each
player. We study, for the first time, the use of *randomized*
strategies in such games. While pure (i.e., nonrandomized) strategies
in timed games require infinite memory for winning even with respect
to reachability objectives, we show that randomized strategies can win
with finite memory with respect to all parity objectives. Also, the
synthesized randomized real-time controllers are much simpler in
structure than the corresponding pure controllers, and therefore
easier to implement. For safety objectives we prove the existence of
pure finite-memory winning strategies. Finally, while randomization
helps in simplifying the strategies required for winning timed parity
games, we prove that randomization does not help in winning at more
states.

*Proceedings of the
11th International Workshop on Hybrid Systems: Computation and Control*
(HSCC),
Lecture Notes in Computer Science 4981,
Springer,
2008,
pp. 87-100.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2008 Springer.