旋转机的形式化建模与分析
计算机科学中的逻辑
2024-07-10 v1
摘要
旋转机具有相当复杂的行为.尤其是在玩家能影响游戏进程的情况下,确定回归率(RTP)往往颇具挑战性.本文使用概率过程规范来建模旋转机的行为,其中玩家的介入通过非确定性来建模.将RTP形式化为一种定量模态公式,可在这些旋转机的行为规范上完全自动地进行评估.我们在Err\`el Industries B.V.提供的实际旋转机上应用了该方法.本文最有用的贡献在于展示了如何既简洁又明确地描述旋转机的行为.通过定量模态逻辑,我们还能轻易提供有价值的见解,例如计算确切的RTP并获得最优玩家策略.
引用
@article{arxiv.2407.06809,
title = {Formal Modelling and Analysis of Slot Machines},
author = {Jan Friso Groote and Sander van Heesch and Matthias Volk},
journal= {arXiv preprint arXiv:2407.06809},
year = {2024}
}