Formal Modelling and Analysis of Slot Machines

TL;DR

This paper models slot machines using probabilistic process specifications with non-determinism to analyze their behavior, compute exact RTP, and derive optimal strategies automatically.

Contribution

It introduces a formal method to describe slot machine behavior concisely and analyze RTP using quantitative modal logic, demonstrated on real machines.

Findings

Accurate modeling of slot machine behavior

Automatic computation of RTP

Identification of optimal player strategies

Abstract

Slot machines can have fairly complex behaviour. Determining the RTP (return to player) can be involved, especially when a player has an influence on the course of the game. In this paper we model the behaviour of slot machines using probabilistic process specifications where the intervention of players is modelled using non-determinism. The RTP is formulated as a quantitative modal formula which can be evaluated fully automatically on the behavioural specifications of these slot machines. We apply the method on an actual slot machine provided by the company Err\`el Industries B.V. The most useful contribution of this paper is that we show how to describe the behaviour of slot machines both concisely and unequivocally. Using quantitative modal logics there is an extra bonus, as we can quite easily provide valuable insights by a.o. computing the exact RTP and obtaining the optimal player strategies.