Теоретические основания программных систем
Научная статья
Проверка бисимуляционной эквивалентности формальных моделей игровых механик с охранными условиями и взвешенными переходами
Влада Владимировна Кугуракова
| Казанский федеральный университет, Казань, Россия | |
|
vlada.kugurakova@gmail.com |
Аннотация.
Настоящая статья посвящена задаче формальной проверки эквивалентности двух реализаций одной игровой механики.
На практике эта задача возникает при рефакторинге игровой логики, сравнении независимых реализаций одной спецификации и верификации балансировочных преобразований.
Для формального представления таких механик используется модель GD-FST
(Game Design Finite State Transducer).
Стандартный подход теории верификации — бисимуляция — здесь неприменим напрямую, поскольку в GD-FST рёбра несут не просто метки, а пары
(условие охраны, вес), что порождает новую нетривиальную задачу согласования переходов.
Вклад работы:
\begin{enumerate}
\item введено определение бисимуляционной эквивалентности для трансдьюсеров GD-FST
(\Altref{определение}{def:bisim}), учитывающее структуру рёбер формализма;
\item предложен алгоритм проверки бисимуляционной эквивалентности (\Altref{алгоритм}{alg:bisim}), построенный на адаптации классического разбиения Канеллакиса–Смолки;
\item доказаны корректность и полнота алгоритма (\Altref{теорема}{thm:corr}).
\end{enumerate}
Практическая значимость результата состоит в возможности автоматической проверки того, что рефакторинг или балансировочное преобразование игровой механики не изменяет её наблюдаемого поведения.
Полученный аппарат применим не только к игровым механикам, но и к другим системам, управляемым правилами с охранными условиями
и числовыми весами.
Ключевые слова: бисимуляционная эквивалентность, GD-FST, игровые механики, верификация, алгоритм Канеллакиса–Смолки, разбиение Хопкрофта, темпоральная логика
Благодарности: Работа выполнена при поддержке Академии наук Республики Татарстан, Соглашение от 22.12.2025 № 12/2025-ПД-КФУ
Для цитирования: Кугуракова В. В. Проверка бисимуляционной эквивалентности формальных моделей игровых механик с охранными условиями и взвешенными переходами // Программные системы: теория и приложения. 2026. Т. 17. № 3. С. 163–190. https://psta.psiras.ru/2026/3_163-190.
Полный текст статьи (PDF): https://psta.psiras.ru/read/psta2026_3_163-190.pdf.
Статья поступила в редакцию 13.07.2026; одобрена после рецензирования 04.08.2026; принята к публикации 17.08.2026; опубликована онлайн 15.09.2026.
