 In this setting, known results about modal logic acquire a new significance. In the realm of finite models, for instance, having the same modal formulas true at two states is equivalent to there being a bisimulation connecting those two states (cf. Blackburn, de Rijke, &amp; Venema 2001). Hence, whenever two finite games satisfy the same modal propositions in their respective roots they are equivalent in the sense of bisimulation. For infinite models, such results are less direct. A full equivalence between bisimulation and satisfying the same formulas, for instance, only holds for an extended modal language with infinite conjunctions and disjunctions. Other relevant results include the existence of modal formulas that define given pointed models up to bisimulation. Such formulas sometimes exist in the basic modal language, sometimes in the μ-calculus, and always in the infinitary modal language. Applied to concrete games G, these modal definitions can be viewed as complete descriptions of all properties of G at the relevant level of invariance.