Visual Modeling of Game Mechanics in Tula: Temporal and Probabilistic Aspects
Main Article Content
Abstract
The paper addresses the problem of visual representation of temporal and probabilistic elements in formal modeling tools for game mechanics. An analysis of existing visual modeling systems – Machinations, Petri nets, UML state diagrams, and UPPAAL – reveals their key limitations in describing complex game scenarios. An approach to visualizing temporal operators and probabilistic constructs in the Tula tool developed by the authors is proposed. A set of visual primitives is described that ensures bidirectional correspondence between visual representation and formal specification in the gameplay specification language. Examples of visual modeling of typical game scenarios with time delays, conditional probabilities, and multiplayer interactions are given. The possibility of automatic transformation of visual models into formal specifications suitable for verification with PRISM and UPPAAL is demonstrated. A comparative analysis of the expressive capabilities of Tula and predecessor systems is conducted, showing that Tula is the only system among those considered that simultaneously provides formally verifiable semantics, built-in support for temporal operators (X, G, F, U), and arbitrary probability distributions, as well as a visual notation organized around resource flows and game events. The two-level specification principle with bidirectional transformation proposed in Tula closes the design–formalization–verification–correction loop, lowering the entry barrier to formal methods for practitioners without loss of verification completeness. This makes it possible to consider Tula as an intermediate layer between iterative game design and industrial verifiers.
Article Details
References
2. Dormans J. Engineering Emergence: Applied Theory for Game Design: dis. … dr. sci. Amsterdam: University of Amsterdam, 2012. 328 p.
3. Kugurakova V.V. Integrating temporal and probabilistic elements into the language of gameplay characteristics // Russian Internet Journal of Industrial Engineering, 2026 (accepted for publication).
4. Rakhmankulova V.R., Kugurakova V.V. Tula Online Tool for Balancing Video Games // Russian Digital Libraries Journal. 2025. Vol. 28, No. 4. P. 903–930.
5. Dormans J. Machinations: Elemental feedback patterns for game design // Proceedings of the 5th International North American Conference on Intelligent Games and Simulation (EUROSIS). 2009. P. 33–40.
6. Dormans J. Simulating mechanics to study emergence in games // Proceedings of the AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment. 2011. Vol. 7, No. 3. P. 2–7.
7. Grünvogel S.M. Formal Models and Game Design // Game Studies. 2005. Vol. 5, No. 1. URL: http://www.gamestudies.org/0501/gruenvogel/
8. Peterson J.L. Petri Net Theory and the Modeling of Systems. Prentice Hall, 1981. 290 p.
9. Molly M.K. Performance Analysis Using Stochastic Petri Nets // IEEE Trans. Comput. 1982. Vol. 31, No. 9. P. 913–917.
10. Martens C. Generative Structural Analysis of Petri Nets // Trans. on Petri Nets and Other Models of Concurrency XI. 2016. P. 37–56.
11. Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Vol. 1. Berlin: Springer, 1997. 234 p.
12. About the Unified Modeling Language Specification Version 2.5.1 // OMG. OMG Unified Modeling Language (OMG UML). URL: https://www.omg.org/spec/UML/2.5.1
13. Segala R. Modeling and Verification of Randomized Distributed Real-Time Systems: dis. … dr. sci. MIT, 1995.
14. Larsen K.G., Pettersson P., Yi W. UPPAAL in a Nutshell // Int. J. Software Tools for Technology Transfer. 1997. Vol. 1, No. 1. P. 134–152.
15. Kwiatkowska M., Norman G., Parker D. PRISM 4.0: Verification of Probabilistic Real-Time Systems // Computer Aided Verification. 2011. P. 585–591.
16. Alur R., Courcoubetis C., Dill D. Model-Checking in Dense Real-Time // Information and Computation. 1993. Vol. 104, No. 1. P. 2–34.
17. Klint P., van Rozen R. Micro-Machinations: A DSL for Game Economies // Software Language Engineering: 6th Int. Conf., SLE 2013, Indianapolis. 2013. Vol. 8225. P. 36–55.
18. Kugurakova V.V. A formal approach to spatio-temporal modeling of game systems // Uchenye Zapiski Kazanskogo Universiteta. Seriya Fiziko-Matematicheskie Nauki. 2024. Vol. 166, No. 4. P. 532–554.
19. Sahibgareeva G.F., Kugurakova V.V., Bolshakov E.S. Game Balance Tools // Russian Digital Libraries Journal. 2023. Vol. 26, No. 2. P. 225–251.
20. Hansson H., Jonsson B. A Logic for Reasoning About Time and Reliability // Formal Aspects of Computing. 1994. Vol. 6, No. 5. P. 512–535.
21. Kaelbling L.P., Littman M.L., Cassandra A.R. Planning and Acting in Partially Observable Stochastic Domains // Artificial Intelligence. 1998. Vol. 101, No. 1–2. P. 99–134.
22. Sicart M. Defining game mechanics // Game studies. 2008. Vol. 8, No. 2. P. 1–14.
23. Pnueli A. The Temporal Logic of Programs // 18th Annual Symposium on Foundations of Computer Science. 1977. P. 46–57.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Presenting an article for publication in the Russian Digital Libraries Journal (RDLJ), the authors automatically give consent to grant a limited license to use the materials of the Kazan (Volga) Federal University (KFU) (of course, only if the article is accepted for publication). This means that KFU has the right to publish an article in the next issue of the journal (on the website or in printed form), as well as to reprint this article in the archives of RDLJ CDs or to include in a particular information system or database, produced by KFU.
All copyrighted materials are placed in RDLJ with the consent of the authors. In the event that any of the authors have objected to its publication of materials on this site, the material can be removed, subject to notification to the Editor in writing.
Documents published in RDLJ are protected by copyright and all rights are reserved by the authors. Authors independently monitor compliance with their rights to reproduce or translate their papers published in the journal. If the material is published in RDLJ, reprinted with permission by another publisher or translated into another language, a reference to the original publication.
By submitting an article for publication in RDLJ, authors should take into account that the publication on the Internet, on the one hand, provide unique opportunities for access to their content, but on the other hand, are a new form of information exchange in the global information society where authors and publishers is not always provided with protection against unauthorized copying or other use of materials protected by copyright.
RDLJ is copyrighted. When using materials from the log must indicate the URL: index.phtml page = elbib / rus / journal?. Any change, addition or editing of the author's text are not allowed. Copying individual fragments of articles from the journal is allowed for distribute, remix, adapt, and build upon article, even commercially, as long as they credit that article for the original creation.
Request for the right to reproduce or use any of the materials published in RDLJ should be addressed to the Editor-in-Chief A.M. Elizarov at the following address: amelizarov@gmail.com.
The publishers of RDLJ is not responsible for the view, set out in the published opinion articles.
We suggest the authors of articles downloaded from this page, sign it and send it to the journal publisher's address by e-mail scan copyright agreements on the transfer of non-exclusive rights to use the work.