On reachability games of ordinal length

Abstract

Games are a classical model in the synthesis of controllers in the open setting. In particular, games of infinite length can represent systems which are not expected to reach a correct state, but rather to handle a continuous stream of events. Yet, even longer sequences of events have to be considered when infinite sequences of events can occur in finite time -Zeno behaviours. In this paper, we extend two-player games to this setting by considering plays of ordinal length. Our two main results are determinacy of reachability games of length less than ωω on finite arenas, and the PSPACE-completeness of deciding the winner in such a game. © Springer-Verlag Berlin Heidelberg 2008.