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.

翻译：老虎机可能具有相当复杂的行为。确定RTP（玩家回报率）可能较为复杂，尤其是在玩家能够影响游戏进程的情况下。本文使用概率过程规约对老虎机行为进行建模，其中玩家干预通过非确定性进行建模。RTP被表述为一种量化模态公式，可以在这些老虎机的行为规约上实现全自动计算。我们将该方法应用于Errèl Industries B.V.公司提供的一台真实老虎机。本文最有价值的贡献在于展示了如何既简洁又明确地描述老虎机行为。使用量化模态逻辑还有一个额外优势：通过计算精确的RTP和获取最优玩家策略等方式，我们能够较为容易地提供有价值的分析见解。