Formal Modeling and Analysis of Slot Machines
Jan Friso Groote, Sander van Heesch, Matthias Volk · IEEE Transactions on Games · 2025
Slot machines can have fairly complex behaviour. Determining theRTP(return to player) can be involved, especially when a player has an influence on the course of the game. In this paper we present a formal model of the behaviour of slot machines and use the model to rigorously and fully automatically compute the RTP. We model the slot machines using probabilistic process specifications where the intervention of players is modelled using non-determinism. The RTP is formulated in quantitative modal logics 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èl 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, among others, computing the exact RTP and obtaining the optimal player strategies.