Model Checking in multiplayer games development

TL;DR

This paper introduces a novel method for applying model checking to verify multiplayer computer games, addressing challenges like state explosion, and demonstrates its application on a case study of Penguin Clash.

Contribution

It presents a new approach to construct game models from descriptions for formal verification using model checking, including a reduction technique to handle state explosion.

Findings

Successful application to Penguin Clash game

Effective model reduction technique developed

Addresses state explosion problem in game verification

Abstract

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.