 These games stand to modal logic in very much the same way as Hintikka’s games stand to first-order logic. In particular they are one way of giving a semantics for modal logic, and they agree with the usual Kripke-type semantics. Of course there are many types and generalisations of modal logic (including closely related logics such as temporal, epistemic and dynamic logics), and so the corresponding games come in many different forms. One example of interest is the computer-theoretic logic of Matthew Hennessy and Robin Milner, used for describing the behaviour of systems; here the arrows come in more than one colour, and moving along an arrow of a particular colour represents performing a particular ‘action’ to change the state. Another example is the more powerful modal \(\mu\)-calculus of Dexter Kozen, which has fixed point operators; see Chapter 5 of Stirling 2001.