Adding probabilistic modeling to executable formal DisCo specifications with applications in strategy modeling in multiplayer game design

Abstract

Formal specifications are software specifications that offer superior accuracy and are based on mathematics. Formal specifications can be written in a predetermined specification language and the specification language can be executable in a way thatmakes it possible to simulate the system specified. A key point when executing the language is the part that is responsible for how the execution proceeds, the execution model.

This work presents a method for using a probabilistic approach to simulate models created as formal specifications with the DisCo software package. The method has been tested by modeling an existing massively multiplayer online game and using the probabilistic approach proposed in this work to simulate player strategies. Tests indicate that the method can be used for modeling strategies based on probabilistic behaviour, and the simulations with these models can give valuable behavioural information, which is useful e.g. in game design.

Key words and phrases: Formal specification, DisCo, probabilistic simulation, game design research