Homepage Program Systems: Theory and Applications Русская версия
ISSN 2079-3316 Bilingual online scientific Online scientific journal of the Ailamazyan Program System Institute of the Ailamazyan PSI of PSI of Russian Academy of Science of RAS 12+ 
Volume 17 (2026) . Issue 3 (72) . Paper No. 5 (515)

Theoretical foundations of software systems

Research Article
DOIDigital Object Identifier 10.25209/2079-3316-2026-17-3-163-190

Checking Bisimulation Equivalence of Formal Game-Mechanic Models with Guard Conditions and Weighted Transitions

Vlada Vladimirovna KugurakovaCorrespondent author

Kazan Federal University, Kazan, Russia
Vlada Vladimirovna Kugurakova — Correspondent author vlada.kugurakova@gmail.com

Abstract. This paper addresses the formal equivalence checking of two implementations of the same game mechanic. Such a task arises in game logic refactoring, comparison of independent implementations of one specification, and verification of balancing transformations. The formal representation of such mechanics is based on the GD-FST (Game Design Finite State Transducer) model. The standard verification-theoretic approach of bisimulation is not directly applicable here, since GD-FST edges carry not mere labels but pairs (guard condition, weight), which generates a novel non-trivial transition-matching problem.
The contribution is as follows: \begin{enumerate} \item a definition of bisimulation equivalence for GD-FST transducers is introduced, accounting for the edge structure of the formalism; \item an algorithm for checking bisimulation equivalence is proposed, constructed by adapting the classical Kanellakis–Smolka partition refinement; \item soundness and completeness of the algorithm are proved. \end{enumerate}
The practical significance of the result lies in enabling automatic verification that refactoring or balancing transformation of a game mechanic does not alter its observable behaviour. The proposed apparatus is applicable not only to game mechanics, but also to other rule-governed systems with guard conditions and numerical weights. (In Russian).

Keywords: bisimulation equivalence, GD-FST, game mechanics, formal verification, Kanellakis–Smolka algorithm, Hopcroft partition, temporal logic

MSC-20202020 Mathematics Subject Classification 68Q85; 68N30, 03B44MSC-2020 68-XX: Computer science MSC-2020 68Qxx: Theory of computing MSC-2020 68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) MSC-2020 68Nxx: Theory of software MSC-2020 68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) MSC-2020 03-XX: Mathematical logic and foundations MSC-2020 03Bxx: General logic MSC-2020 03B44: Temporal logic

For citation: Vlada V. Kugurakova. Checking Bisimulation Equivalence of Formal Game-Mechanic Models with Guard Conditions and Weighted Transitions. Program Systems: Theory and Applications, 2026, 17:3, pp. 163–190. (In Russ.). https://psta.psiras.ru/2026/3_163-190.

Full text of article (PDF): https://psta.psiras.ru/read/psta2026_3_163-190.pdf.

The article was submitted 13.07.2026; approved after reviewing 04.08.2026; accepted for publication 17.08.2026; published online 15.09.2026.

© Kugurakova V. V.
2026
Editorial address: Ailamazyan Program Systems Institute of the Russian Academy of Sciences, Peter the First Street 4«a», Veskovo village, Pereslavl area, Yaroslavl region, 152021 Russia;   Website:  http://psta.psiras.ru Phone: +7(4852) 695-228;   E-mail: ;   License: CC-BY-4.0License text on the Creative Commons site
© Ailamazyan Program System Institute of Russian Academy of Science (site design) 2010–2026