{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:18:46Z","timestamp":1766132326210,"version":"3.48.0"},"reference-count":41,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Games"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1109\/tg.2025.3594957","type":"journal-article","created":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T18:16:58Z","timestamp":1754072218000},"page":"1070-1083","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling and Analysis of Slot Machines"],"prefix":"10.1109","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2196-6587","authenticated-orcid":false,"given":"Jan Friso","family":"Groote","sequence":"first","affiliation":[{"name":"Formal System Analysis Group, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-9719-3559","authenticated-orcid":false,"given":"Sander","family":"van Heesch","sequence":"additional","affiliation":[{"name":"Formal System Analysis Group, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[{"name":"Formal System Analysis Group, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"year":"2024","key":"ref1","article-title":"Regulations regarding slot machines, part of the Dutch Civil Code"},{"year":"2025","key":"ref2","article-title":"Spelen op EEN speelautomaat"},{"volume-title":"Principles of Model Checking","year":"2008","author":"Baier","key":"ref3"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/2933575.2934574","article-title":"The probabilistic model checking Landscape","volume-title":"Proc. 31st Annu. ACM\/IEEE Symp. Log. Comput. Sci.","author":"Katoen","year":"2016"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9946.001.0001"},{"key":"ref7","article-title":"A Calculus of Communicating Systems","volume":"92","author":"Milner","year":"1980"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.034"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78089-0_15"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00633-z"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"ref14","first-page":"28:1","article-title":"Real equation systems with alternating fixed-points","volume":"279","author":"Groote","year":"2023","journal-title":"CONCUR"},{"article-title":"JVH gaming marktleider met voorbeeldfunctie","year":"2025","author":"Gaming\/Errl","key":"ref15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90183-G"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.103.6"},{"volume-title":"The Mathematics of Slots: Configurations, Combinations, Probabilities","year":"2013","author":"Barboianu","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1080\/14459790802405889"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26520-9_22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15585-2_6"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57099-0_45"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1155\/2021\/8784065"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013689704352"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-49819-5_6"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75775-4_4"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1137\/140983781"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1080\/0025570x.2003.11953165"},{"article-title":"Modeling and analyzing board games through Markov decision processes","year":"2023","author":"Mocanu","key":"ref29"},{"article-title":"Modeling and analysis of the board game Mythic Battles: Pantheon through Markov decision processes","year":"2025","author":"Otte","key":"ref30"},{"article-title":"Using probabilistic model checking to balance games","year":"2021","author":"Kavanagh","key":"ref31"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10003-2_79"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_21"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1961204.1961207"},{"year":"2025","key":"ref35","article-title":"Topspinner"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_17"},{"key":"ref37","first-page":"86","article-title":"Evidence extraction from parameterised Boolean equation systems","volume-title":"Proc. Int. Workshop Automated Reasoning Quantified Non-Classical Log.","author":"Wesselink","year":"2018"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_8"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00633-z"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00442-x"}],"container-title":["IEEE Transactions on Games"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/7782673\/11301972\/11106697.pdf?arnumber=11106697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:14:13Z","timestamp":1766132053000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11106697\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":41,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tg.2025.3594957","relation":{},"ISSN":["2475-1502","2475-1510"],"issn-type":[{"type":"print","value":"2475-1502"},{"type":"electronic","value":"2475-1510"}],"subject":[],"published":{"date-parts":[[2025,12]]}}}