A formal approach to spatio-temporal modeling of game systems

   This article introduces FAST-GM (Formal Approach to Spatio-Temporal Game Modeling), a new unified approach to formal modeling of game entities and their interactions that integrates temporal and probabilistic dimensions, thus offering a comprehensive framework for capturing the dynamics of game systems. Built upon the principles of extended temporal logic and probability theory, FAST-GM accurately describes complex game mechanics and how they evolve. A formal definition of game entities was considered. Their states and interactions were explored. The methods for integrating temporal and probabilistic elements into gameplay were discussed. The applicability of FAST-GM for game balancing, formal verification of game scenarios, and automated generation of test cases was analyzed. Its scalability and adaptability in various game genres were assessed. The results obtained show that FAST-GM should advance the formal modeling of game systems, equipping developers with a powerful toolset for analysis, verification, and optimization of game mechanics throughout the process of creating a video game.

1. Sahibgareeva G.F., Kugurakova V.V., Bolshakov E.S. Video game’s mechanics generation and balancing. Nauch. servis v seti Internet : tr. XXIV Vseros. nauch. konf. (19–22 sent. 2022 g., onlain) [Scientific Service & Internet : Proc. XXIV All-Russ. Sci. Conf. (September 19–22, 2022, Online)]. Moscow, IPM im. M.V. Keldysha, 2022, pp. 455–485. doi: 10.20948/abrau-2022-6. (In Russian)

2. Sahibgareeva G.F., Kugurakova V.V. Game balance practices. Program. Sist.: Teor. Prilozh., 2022, vol. 13, no. 3, pp. 255–273. doi: 10.25209/2079-3316-2022-13-3-255-273. (In Russian)

3. Nurlygaianov N.R., Kugurakova V.V. A new approach to creating a corpus of video game texts. Elektron. Bibl., 2024, vol. 27, no. 4, pp. 587–597. doi: 10.26907/1562-5419-2024-27-4-578-597. (In Russian)

4. Levenchuk A. Sistemnoe myshlenie [Systems Thinking]. Vol. 1. Yekaterinburg, Ridero, 2024. 412 p. (In Russian)

5. Aarseth E. Computer game studies, year one. Game Stud., 2001, vol. 1, no. 1.

6. Juul J. Half-Real: Video Games between Real Rules and Fictional Worlds. Cambridge, MA, MIT Press, 2005. 248 p.

7. Mateas M., Stern A. Structuring content in the fa¸cade interactive drama architecture. Proc. Artif. Intell. Interact. Digital Entertainment Conf., 2005, vol. 1, no. 1, pp. 93–98. doi: 10.1609/aiide.v1i1.18722.

8. Nelson M.J., Mateas M. Towards a formal game grammar. Proc. 6^th Int. Conf. on Cognitive Modeling, 2008, pp. 137–143.

9. Zagal J.P., Mateas M., Fern´andez-Vara C., Hochhalter B., Lichti N. Towards an ontological language for game analysis. Proc. DiGRA 2005 Conf.: Changing Views – Worlds in Play. Tampere, DiGRA, 2005, pp. 1–13.

10. Cook D. The chemistry of game design. Game Developer. 2007. URL: https://www.gamedeveloper.com/design/the-chemistry-of-game-design.

11. Bj¨ork S., Holopainen J. Patterns in Game Design. Ser.: Game Development Series. Hingham, MA, Charles River Media, 2005. xvii, 423 p.

12. Brogi A., Canciani A., Soldani J., Wang P. A Petri net-nased approach to model and analyze the management of cloud applications. In: Koutny M., Desel J., Kleijn J. (Eds.) Transactions on Petri Nets and Other Models of Concurrency XI. Ser.: Lecture Notes in Computer Science. Berlin, Heidelberg, Springer, 2016, pp. 28–48. doi: 10.1007/978-3-662-53401-4_2.

13. Gr¨unvogel S.M. Formal models and game design. Game Stud., 2005, vol. 5, no. 1.

14. Rakhmankulova V., Kugurakova V. Developing an online tool for balancing video games. Proc. Int. Conf. on Simplicity and Complexity in SMART Automatics and Energy Systems (SMART-SYSTEMS), 2024, pp. 1–6.

15. Pnueli A. The temporal logic of programs. Proc. 18th Annu. Symp. on Foundations of Computer Science (sfcs 1977). Providence, RI, IEEE, 1977, pp. 46–57. doi: 10.1109/SFCS.1977.32.

16. Ross S.M. Introduction to Probability Models. 12^th ed. Acad. Press, 2019. 842 p. doi: 10.1016/C2017-0-01324-1.

17. Hansson H., Jonsson B. A logic for reasoning about time and reliability. Formal Aspects Comput., 1994, vol. 6, no. 5, pp. 512–535. doi: 10.1007/BF01211866.

18. Apperley T.H. Genre and game studies: Toward a critical approach to video game genres. Simul. Gaming, 2006, vol. 37, no. 1, pp. 6–23. doi: 10.1177/1046878105282278.

19. Nilsson N.J. Probabilistic logic. Artif. Intell., 1986, vol. 28, no. 1, pp. 71–87. doi: 10.1016/0004-3702(86)90031-7.

20. Fagin R., Halpern J.Y., Megiddo N. A logic for reasoning about probabilities. Inf. Comput., 1990, vol. 87, nos. 1–2, pp. 78–128. doi: 10.1016/0890-5401(90)90060-U.

21. Sistla A.P., Clarke E.M. The complexity of propositional linear temporal logics. J. ACM, 1985, vol. 32, no. 3, pp. 733–749. doi: 10.1145/3828.3837.

22. Papadimitriou C.H. Games against nature. J. Comput. Syst. Sci., 1985, vol. 31, no. 2, pp. 288–301. doi: 10.1016/0022-0000(85)90045-5.

23. Biere A., Cimatti A., Clarke E., Zhu Y. Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99): Proc. 5^th Int. Conf. Cleaveland W.R. (Ed.). Ser.: Lecture Notes in Computer Science. Vol. 1579. Berlin, Heidelberg, Springer, 1999, pp. 193–207. doi: 10.1007/3-540-49059-0_14.

24. Biere A., Heljanko K., Junttila T., Latvala T., Schuppan V. Linear encodings of bounded LTL model checking. Logical Methods Comput. Sci., 2006, vol. 2, no. 5, pp. 1–64. doi: 10.2168/LMCS-2(5:5)2006.

25. Henriques D., Martins J.G., Zuliani P., Platzer A., Clarke E.M. Statistical model checking for Markov decision processes. Proc. 2012 9^th Int. Conf. on Quantitative Evaluation of Systems. London, IEEE, 2012, pp. 84–93. doi: 10.1109/QEST.2012.19.