  Multiplayer computer games play a big role in the ever-growing entertainment
industry. Being competitive in this industry means releasing the best possible
software, and reliability is a key feature to win the market. Computer games
are also actively used to simulate different robotic systems where reliability
is even more important, and potentially critical. Traditional software testing
approaches can check a subset of all the possible program executions, and they
can never guarantee complete absence of errors in the source code. On the other
hand, during more than twenty years, Model Checking has demonstrated to be a
powerful instrument for formal verification of large hardware and software
components. In this paper, we contribute with a novel approach to formally
verify computer games. We propose a method of model construction that starts
from a computer game description and utilizes Model Checking technique. We
apply the method on a case study: the game Penguin Clash. Finally, an approach
to game model reduction (and its implementation) is introduced in order to
address the state explosion problem.
