Model Checking for mobile game development and analysis

Context: The video game industry has seen a huge uptake in mobile games, and for the first time mobile games are set to become the largest sector, projected to make up 37% of the entire market by 2016 by Newzoo , a leading market intelligence firm specialising in video games. Free-to-play titles provide a very different model to those seen by more traditional models such as pay-to-play games. By removing the financial barrier of entry to free-to-play titles, developers hope to get more people downloading their games and to encourage them to pay for in-app purchases. The actual game aspect of these titles is often minimal, making up a very small proportion of the player's game time. Instead players spend the majority of their time in the "metagame"; that is, all activities that surround the game itself. These activities take several forms such as rules governing player progression, level unlocks, purchasing and equipping upgrades, earning and spending currency etc. Games developers are keen to analyse mobile games users' behaviour in order to maximise profit. In this project we investigate how Model Checking can be used to do this analysis.

Model checking is a technique that allows for the automated analysis and verification of complex systems. It involves creating a mathematical model of the possible behaviours of each component system. A model checker can be used to create a model combining the interleaving behaviours of all components of the system, and to explore this model to check properties of the system. Properties can be qualitative (e.g. all players will eventually reach level 6) or quantitative (e.g. the expected number of upgrades for a player within 5 days is 7).

Aims and objectives: The main aim of the project is to develop theories and software to allow the use of model checking for game design and testing

The objectives are to:
- establish the state of the art in this field
- create models of user behaviour for testing
- develop industrial collaborators (for case studies/data)
- develop software for games developers with in-built verification machine
- develop models of user behaviour for in-game economy optimisation

Novelty: The recent emergence of free-to-play titles and their respective meta-games has not been widely studied, and for that reason is poorly understood. Only a very small proportion of the player-base needs to make any purchases in order for developers to make money. In a report by SWRVE, a mobile marketing firm, it was found that fewer than 2% of users made in-app purchases. In the competitive mobile games market, where margins are so small, any way to maximise income for the developers will be highly desirable.

Alignment with EPSRC strategies and research areas: Aligns with EPSRC strategy on Novel Computation and Mathematical Sciences (Integration, analysis and interpretation of data for decision making; and in silico modelling and simulation), and with EPSRC research areas: artificial intelligence technologies, logic and combinatorics, and verification and correctness.

Potential Applications: Mobile game development.

Potential Companies/collaborations: Companies - Studio Gobo (Brighton), Glasgow Neural Ltd. (Glasgow), Tag Games (Dundee).