Визуальное моделирование игровых механик в инструменте Tula: темпоральные и вероятностные аспекты
Main Article Content
Аннотация
Рассмотрена проблема визуального представления темпоральных и вероятностных элементов в инструментах формального моделирования игровых механик. На основе анализа существующих систем визуального моделирования – Machinations, сетей Петри, диаграмм состояний UML и UPPAAL – выявлены их ключевые ограничения при описании сложных игровых сценариев. Предложен подход к визуализации темпоральных операторов и вероятностных конструкций в инструменте Tula, разработанном авторами. Описан набор визуальных примитивов, обеспечивающих двунаправленное соответствие между визуальным представлением и формальной спецификацией на языке геймплея. Приведены примеры визуального моделирования типовых игровых сценариев с элементами временных задержек, условных вероятностей и многопользовательских взаимодействий. Показана возможность автоматической трансформации визуальных моделей в формальные спецификации, пригодные для верификации средствами PRISM и UPPAAL. Проведён сравнительный анализ выразительных возможностей Tula и систем-предшественников, показавший, что Tula является единственной из рассмотренных систем, одновременно обеспечивающей формальную верифицируемую семантику, встроенную поддержку темпоральных операторов (X, G, F, U) и произвольных вероятностных распределений, а также визуальную нотацию, организованную вокруг ресурсных потоков и игровых событий. Предложенный в Tula принцип двухуровневой спецификации с двунаправленной трансформацией замыкает цикл «дизайн → формализация → верификация → корректировка», снижая порог входа в формальные методы для практиков без потери верификационной полноты. Это позволяет рассматривать Tula как промежуточный слой между итеративным геймдизайном и промышленными верификаторами.
Article Details
Библиографические ссылки
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.
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Представляя статьи для публикации в журнале «Электронные библиотеки», авторы автоматически дают согласие предоставить ограниченную лицензию на использование материалов Казанскому (Приволжскому) федеральному университету (КФУ) (разумеется, лишь в том случае, если статья будет принята к публикации). Это означает, что КФУ имеет право опубликовать статью в ближайшем выпуске журнала (на веб-сайте или в печатной форме), а также переиздавать эту статью на архивных компакт-дисках журнала или включить в ту или иную информационную систему или базу данных, производимую КФУ.
Все авторские материалы размещены в журнале «Электронные библиотеки» с ведома авторов. В случае, если у кого-либо из авторов есть возражения против публикации его материалов на данном сайте, материал может быть снят при условии уведомления редакции журнала в письменной форме.
Документы, изданные в журнале «Электронные библиотеки», защищены законодательством об авторских правах, и все авторские права сохраняются за авторами. Авторы самостоятельно следят за соблюдением своих прав на воспроизводство или перевод их работ, опубликованных в журнале. Если материал, опубликованный в журнале «Электронные библиотеки», с разрешения автора переиздается другим издателем или переводится на другой язык, то ссылка на оригинальную публикацию обязательна.
Передавая статьи для опубликования в журнале «Электронные библиотеки», авторы должны принимать в расчет, что публикации в интернете, с одной стороны, предоставляют уникальные возможности доступа к их материалам, но, с другой, являются новой формой обмена информацией в глобальном информационном обществе, где авторы и издатели пока не всегда обеспечены защитой от неправомочного копирования или иного использования материалов, защищенных авторским правом.
При использовании материалов из журнала обязательна ссылка на URL: http://rdl-journal.ru. Любые изменения, дополнения или редактирования авторского текста недопустимы. Копирование отдельных фрагментов статей из журнала разрешается для научных исследований, персонального использования, коммерческого использования до тех пор, пока есть ссылка на оригинальную статью.
Запросы на право переиздания или использования любых материалов, опубликованных в журнале «Электронные библиотеки», следует направлять главному редактору Елизарову А.М. по адресу: amelizarov@gmail.com
Издатели журнала «Электронные библиотеки» не несут ответственности за точки зрения, излагаемые в публикуемых авторских статьях.
Предлагаем авторам статей загрузить с этой страницы, подписать и выслать в адрес издателя журнала по электронной почте скан Авторского договора о передаче неисключительных прав на использование произведения.