Modelling and Exploring Rules of Play in a Board Game for Social Computing


Can I play a board game with friends and help solve a complex scientific problem or acheive social mobilization? This is the general question that intrigues us. Lets take a look at social mobilization. It is a process that engages and motivates a wide range of people to raise awareness of and demand for a particular development and/or educational objective. For instance, raising awareness about the Humanpapillonoma Virus (HPV) requires people to understand concepts such as epithelial cells, warts, cancer cells, the different strains of the HPV viruses, and  treatment techniques. People also need to understand the relationship between these concepts and share information that they think is new and relevant with their friends. We developed FightHPV, a mobile board game, that represents concepts as characters and the characters have relationships to each other such as an epithelial cell can be infected by a wart. The game has a set of board game rules, an initial state and a desired final board state or final board condition. The game engages players into understanding concepts and their relationships by moving the pieces around until they reach the desired final condition and consequently gain points. Information conveyed in the game helps raise awareness about HPV.

The masters thesis will use the board game setup of FightHPV to address some fundamental questions about gamification. The student will model the game and the rules of the game as constraints in a formal modelling language, such as Alloy [1]. The solutions to the model are essentially the moves to go from an initial board state to a final board state/condition. Solving the formal model will help determine the difficulty of each level. Higher the number of solutions easier the level and it gets harder as the number of solutions is fewer. The student will design levels based on exploring the solution space of the formal model. The idea is to use the board game framework to train (warm-up) people into first solving constraints with known solutions and ultimately having them solve problems that are intractable or NP-hard, hence, leveraging the reasoning abilities of humans for social computing. The thesis will also explore the possibility of mapping other scientific/social mobilization problems as a board game. See references for more information.


Develop a formal model in Alloy for a mobile board game and map a scientific challenge/social mobilization problem to it. Explore the solution space of the formal model to design levels.

Learning outcome:

  • Conducting a literature review
  • Scientific writing
  • Alloy for formal modelling
  • Gamification/social computing


  • Bachelor’s degree in computer science
  • Good communication skills and ability to work in a team
  • Interest in formal modelling and theoretical computer science

Contact persons:

Sagar Sen, Research Scientist, Simula Research Laboratory. Email:
Tomas Ruiz Lopez, Postdoc, Cancer Registry of Norway. Email:
Michael Riegler, PhD Candidate, Simula Research Laboratory. Email:


[1] Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press.
[2] Soduku in Alloy
[3] Hersher, Rebecca (April 13, 2012). "FoldIt game’s next play: crowdsourcing better drug design". Retrieved April 16, 2012.
[4] Waqas Moazzam, Michael Riegler, Sagar Sen, Mari Nygård: Scientific Hangman: Gamifying Scientific Evidence for General Public. GamifIR@ECIR 2015: 26-33
[5] Niklas Een et. al. SAT-based Strategy Extraction in Reachability Games