 Infinite games So far, games were tacitly assumed finite in length. This assumption is innocuous for many real life scenarios, yet there are notable exceptions. A prominent example are safety games, where one of the players, the guard, has to ensure a system to never leave a certain state, while the opponent attempts to deviate. Many technical tools for finite games also work for infinite games. There is, however, a number of conceptual and logical discontinuities. Since infinite games have no last moments, for instance, outcomes must be attached to complete histories of game play, rather than leaves of a tree. Reasoning about games then requires temporal modalities for a given history, but also modalities ranging over all open future histories. For analyzing powers, then, temporal versions of forcing modalities are needed. With these modifications, a logical style of analysis still applies. For instance, it is well-known that determinacy fails for infinite games (Jech 2003). However, what holds for all games is a law of ‘weak determinacy’ stating that, if i has no strategy to force a set of histories satisfying \(\varphi\), her opponent j can ensure that i will never obtain such a \(\varphi\)-strategy in the future. The difference between standard determinacy and weak determinacy is captured by the following two formulas, that are entirely in line with this section’s style of analysis: \(\{i\}\varphi\,\lor\,\{j\}\neg\varphi\) (determinacy) versus \(\{i\}\varphi\lor\{j\}G\neg\{i\}\varphi\) (weak determinacy), where G is the temporal modality of ‘always in the future on the current history’. A more radical use of infinite games is found in coalgebra (Abramsky 1997; Jacobs 2016), where infinite processes are modeled that can only be observed from the outside, but not built up finitely from ground elements.