Model Checking for mobile game development and analysis

内容：视频游戏行业已经看到了手机游戏的巨大增长，并且手机游戏将首次成为最大的行业，Newzoo是一家专注于视频游戏的领先市场情报公司，预计到2016年将占整个市场的37%。免费游戏提供了一个非常不同的模式，以那些更传统的模式，如付费游戏。通过消除进入免费游戏的财务障碍，开发人员希望让更多的人下载他们的游戏，并鼓励他们为应用内购买付费。这些游戏的实际游戏方面通常是最小的，只占玩家游戏时间的一小部分。相反，玩家将大部分时间花在“元游戏”上，即围绕游戏本身的所有活动。这些活动采取多种形式，如规则管理玩家的进展，水平解锁，购买和装备升级，赚取和消费货币等游戏开发商热衷于分析手机游戏用户的行为，以最大限度地提高利润。在这个项目中，我们将研究如何使用模型检查来进行分析。模型检查是一种允许对复杂系统进行自动分析和验证的技术。它涉及创建每个组成系统的可能行为的数学模型。模型检查器可以用来创建一个模型，结合系统的所有组件的交错行为，并探索这个模型来检查系统的属性。属性可以是定性的（例如所有玩家最终都会达到6级）或量化（例如，玩家在5天内的预期升级次数为7次）。目的和目标：该项目的主要目的是开发理论和软件，以便在游戏设计和测试中使用模型检查。- 建立该领域的最新技术-创建用户行为模型进行测试-开发行业合作伙伴（用于案例研究/数据）-为游戏开发商开发内置验证机的软件-为游戏内经济优化开发用户行为模型新颖性：最近出现的免费游戏及其相应的元游戏尚未得到广泛研究，因此人们对此知之甚少。只有一小部分玩家需要购买游戏才能让开发者赚钱。移动的营销公司SWRVE的一份报告发现，只有不到2%的用户进行了应用内购买。在竞争激烈的手机游戏市场，利润率是如此之小，任何方法，以最大限度地提高收入的开发商将是非常可取的。与EPSRC的战略和研究领域一致：与EPSRC的战略一致的新计算和数学科学（决策数据的整合、分析和解释;以及计算机建模和模拟），以及EPSRC研究领域：人工智能技术、逻辑和组合学、验证和正确性。潜在应用：移动的游戏开发。潜在公司/合作：公司-Studio Gobo（布莱顿）、格拉斯哥神经有限公司（格拉斯哥）、Tag Games（邓迪）。

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 testingThe 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 optimisationNovelty: 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).