 This result of Rabin is one of several influential resuls that connect games with automata. Another example is the parity games which are used for verifying properties of modal systems. See for example Stirling (2001) Chapter 6; Bradfield and Stirling (2006) discuss parity games for the modal \(\mu\)-calculus. 