Проверка бисимуляционной эквивалентности формальных моделей игровых механик с охранными условиями и взвешенными переходами

Одной из фундаментальных задач инженерии программного обеспечения является обеспечение поведенческой эквивалентности систем при их модификации, оптимизации или рефакторинге. В области разработки видеоигр эта проблема приобретает особую остроту из-за высокой итеративности геймдизайна и растущей сложности внутренних взаимосвязей механик.

Игровая механика может быть реализована по-разному, сохраняя при этом идентичное наблюдаемое поведение. Классический пример: кулдаун, реализованный через непрерывный таймер, и кулдаун, реализованный через дискретный счётчик тиков (тактов игрового процесса), могут быть интуитивно неотличимы для игрока, однако формальная проверка такой эквивалентности требует явного согласования словарей переменных и переходов фаз ACTIVE → COOLDOWN → READY . Без такого согласования две реализации могут оказаться различимы на уровне охранных условий. Аналогичная ситуация возникает при рефакторинге игровой логики в редакторе Tula [1] : геймдизайнер переструктурировал механику, и требуется гарантия, что новая реализация поведенчески эквивалентна исходной.

В теории верификации программ задача поведенческой эквивалентности решается через бисимуляцию [2, 3] : два автомата бисимулярны, если каждый переход в одном может быть «зеркально» воспроизведён в другом, и наоборот. Бисимулярные системы удовлетворяют одним и тем же формулам темпоральных логик CTL (Computation Tree Logic — логика деревьев вычислений) [4] и LTL (Linear Temporal Logic — линейная темпоральная логика) [5 , 6] , что делает бисимуляцию мощным инструментом верификации.

Переход от игровой механики к формальной модели. В настоящей работе игровая механика рассматривается как конечная графовая модель поведения: вершины задают наблюдаемые фазы или конфигурации механики, а рёбра — допустимые переходы между ними, вызываемые действиями игрока, системными событиями или изменениями параметров среды. Такой взгляд позволяет сравнивать не конкретный код в игровом движке, а абстрактное поведение механики.

Для такого представления используется ориентированный конечный граф состояний и переходов, дополненный разметкой вершин, охранными условиями и числовыми весами переходов, — называемый трансдьюсером GD-FS T 1 . Формальное определение GD-FST приведено в определении 2.

Нетривиальность проверки эквивалентности. После перехода к графовой модели задача не сводится к проверке изоморфизма графов. Стандартная бисимуляция определена для размеченных систем переходов с помеченными рёбрами [2] , однако в GD-FST рёбра несут составные метки (cond, w) G Cond x R > q , где cond — булево условие охраны, w — числовой вес перехода. Это порождает три нетривиальных вопроса, не возникающих в стандартной теории:

• ( 1 )    Когда два перехода (v 1 , e ₁ ,v ^, ₁ ) и (v ₂ , e ₂ , v 2 ) считаются «согласованными»?

• ( 2 )    Как сравнивать логически эквивалентные, но синтаксически различные условия охраны?

• ( 3 )    Как трактовать вероятностные веса при проверке стохастической эквивалентности?

2. Предварительные сведения 2.1. Обозначения

Настоящая статья отвечает на эти вопросы, вводя GD-бисимуляцию — расширение классического понятия, специализированное для моделей игровых механик с охранными условиями и взвешенными переходами.

Существующие инструменты и их ограничения. Дорманс [7] предложил диаграммы Machinations — графический формализм с операционной семантикой для моделирования потоков ресурсов в игровых механиках; днако этот аппарат ориентирован на симуляцию и балансировку и не поддерживает ни формальную верификацию, ни проверку поведенческой эквивалентности реализаций. Обзор методов software model checking применительно к игровым движкам [8] показывает, что существующие подходы ориентированы на верификацию кода реализации, а не игровой логики, и не предоставляют формального аппарата для сравнения двух реализаций одной спецификации. Таким образом, задача GD-бисимуляции возникает в предметной области, где существующие инструменты оставляют формальный пробел.

Множественность семантик. Один и тот же GD-FST допускает несколько устоявшихся семантик в зависимости от вопроса верификации: как раскрашенная сеть Петри он поддаётся анализу параллелизма и достижимости, как цепь Маркова (DTMC/MDP) — вероятностной проверке в PCTL/CSL, как сеть временны´ х автоматов — анализу с временными ограничениями в TCTL (Timed Computation Tree Logic), то есть временн´ом расширении CTL для систем с часами. Этот список не является исчерпывающим: возможны и другие интерпретации — например, взвешенный автомат над полукольцом для количественного анализа путей или стохастическая игра для синтеза стратегий.

Каждая такая семантическая интерпретация заимствует доказательную базу зрелой теории. Возможность изучать одну и ту же формальную модель через различные поведенческие семантики отражает устоявшийся методологический принцип формальных методов [9]. Настоящая работа использует интерпретацию GD-FST как размеченной системы переходов 2, а её алгоритмика восходит к минимизации конечных автоматов [10]. Именно это позволяет перенести классический аппарат без изменения его сути, адаптировав понятие согласованности переходов к составным меткам (cond, w).

Вклад и позиционирование. Работа относится к теоретическому фундаменту формальных методов анализа игровых механик и решает самостоятельную задачу в рамках класса K5 (поведенческая эквивалентность) классификации задач формального анализа игровых систем [11] — проверку бисимуляционной эквивалентности моделей GD-FST. Она примыкает к линии работ автора по формальным методам в геймдизайне [12, 13] , оставаясь при этом законченным независимым исследованием: вводимые определения, алгоритм и доказательства самодостаточны и не опираются на результаты этих работ.

Переносимость. Введённые определения и алгоритм применимы к любым размеченным системам переходов с охранными условиями и числовыми весами: сетевым протоколам, рабочим процессам (workflow), мультиагентным системам. Игровые механики служат основным, но не единственным примером.

В таблице 1 собраны основные обозначения, используемые в статье.

	Таблица 1. Основные обозначения
Обозначение	Смысл

T = (V,E,X V ,X _E ) GD-FST трансдьюсер

(T ,v o ) a v -→ v ′ cond i = cond 2 e 1 ≃ e 2 v 1 ∼ v 2 T 1 ∼ T 2 P i P ∗

отмеченный трансдьюсер с начальной вершиной v 0 переход по метке a логическая эквивалентность условий охраны (cond , w ) -coBMecTUMOCTb рёбер (определение 5) GD-бисимулярность вершин (определение 6) GD-бисимулярность отмеченных трансдьюсеров разбиение на i -й итерации алгоритма стабилизированное разбиение

² LTS — Label led Transition System , размеченная, или маркированная, система переходов: формальная модель поведения, в которой переходы между состояниями снабжены метками действий, событий или условий наблюдения. Формальное определение используется в разделе 2.3.

• 2.2.    Игровая механика и GD-FST трансдьюсер

Определение 1 (Игровая механика). Игровой механикой называется правило, регулирующее взаимодействие игрока с игровой системой: оно описывает, при каких условиях действие доступно, каков его эффект и какова его стоимость [7] .

Чтобы проверять эквивалентность механик формально, далее игровая механика рассматривается как конечная графовая модель: вершины соответствуют фазам механики, а рёбра — переходам между фазами, помеченным условиями применимости и числовыми параметрами перехода. Такую модель фиксирует следующий формализм.

Определение 2 (GD-FST трансдьюсер [1, 14] ). GD-FST трансдью-сером (Game Design Finite State Transducer — конечный трансдьюсер состояний игрового дизайна) называется четвёрка T = (V, E, Х у , Х е ), где V — непустое конечное множество вершин (игровых состояний); E С V х V — множество рёбер (переходов); Х у : V ч Л у — функция разметки вершин наблюдаемыми метками состояний, где Л у — конечное множество таких меток; Х е : E ^ Cond х R > o — функция пометки рёбер условием охраны и весом.

В простейшем ролевом варианте Л у может включать метки source , transform и terminal : source обозначает порождающую (входную) вершину, transform — промежуточную преобразующую фазу, terminal — завершающую (поглощающую) вершину. (В прикладных моделях игровых механик Л у может быть богаче и включать фазовые метки, например READY , ACTIVE , COOLDOWN .) Терминальные вершины, если они нужны в конкретной модели, задаются разметкой: V w = {v G V : Х у (v) = terminal}.

Вес w ∈ R ≥ 0 допускает две интерпретации: детерминированную (стоимость, урон, длительность), при которой согласование весов есть точное равенство w 1 = w ₂ , и стохастическую (вероятность перехода) при дополнительном условии нормировки ^v‘ w(v,v ' ) = 1 в каждой вершине; стохастический случай подробно разобран в Замечании 3 .

Для проверки эквивалентности механик далее рассматривается отмеченный GD-FST трансдьюсер (T , v ₀ ), где v ₀ G V — начальная вершина, или стартовая фаза механики. Если начальные вершины ясны из контекста, запись T ₁ ∼ T ₂ используется как сокращение для GD-бисимулярности отмеченных трансдьюсеров (7 1 ,v 1 ) и (7 2 , v 2 ).

В рамках этого формализма конкретная игровая механика задаётся отмеченным фрагментом GD-FST: набором вершин (фаз механики) и рёбер (переходов между фазами) с пометками условий охраны и весами λ E .

Объект T называется трансдьюсером , а не просто графом, поскольку несёт двойную разметку: λ V фиксирует типы состояний, λ E — условия срабатывания и веса переходов. Трансдьюсерная природа проявляется в том, что механика сопоставляет входному состоянию среды, проверяемому охранами, наблюдаемый переход с количественной характеристикой w. Собственно эффекты переходов остаются в объемлющем формализме FAST-GM и в данной работе абстрагируются.

Семантика среды. Охранные условия cond ∈ Cond суть предикаты над конечным множеством переменных среды Var (таймеры, счётчики, ресурсы, флаги состояния; например, Var = {timer, ticks, mana, hp}), которым сопоставлена глобальная оценка η, приписывающая каждой переменной значение из её домена. Ребро e с меткой A e (e) = (cond,w) проходимо в оценке п, если п = cond. Сами переменные, их домены и функции обновления (эффекты переходов) принадлежат объемлющему формализму сущностей FAST-G M3 [14] , по отношению к которому GD-FST является проекцией управляющей структуры : трансдьюсер фиксирует фазы механики и условия и веса переходов между ними, абстрагируясь от конкретной динамики переменных. Соответственно GD-бисимуляция (определение 6) определяется на управляющем уровне относительно фиксированной разделяемой семантики среды : оба сравниваемых трансдьюсера интерпретируются над общим словарём Var с общей динамикой η.

• 2.3.    Классическая бисимуляция

Понятие бисимуляции введено Парком [3] и развито Милнером [2] в контексте теории параллельных процессов — CCS (Calculus of Communicating Systems, исчисление взаимодействующих систем) [2] . Для размеченных систем переходов оно определяется следующим образом.

Определение 3 (Размеченная система переходов (LTS)). Размеченной системой переходов (Labelled Transition System, LTS) в настоящей работе называется четвёрка

S = (S, A, ^,1), где S — множество состояний, A — алфавит меток переходов, → ⊆ S ×A× S — отношение переходов, а I : S ^ Л — функция разметки состояний. Запись s -a- s' означает, что (s, a, s') G ^.

Определение 4 (Бисимуляция [2, 3] ). Бинарное отношение R ⊆ S × S называется бисимуляцией на размеченной системе переходов S = (S, A, д ,1), если для любых s _i ,s ₂ с (s _i ,s ₂ ) £ R:

• ( i )    l(s 1 ) = l(s ₂ ) (совпадение меток состояний);

• ( ii )    для любого перехода s _i -д s i существует s ₂ -д s 2 такой, что (s i , s 2 ) G R;

• 2.4.    Алгоритм Канеллакиса–Смолки

im) симметрично: для любого s ₂ Д s 2 существует s _i Д s i с (s i , s 2 ) G R.

Состояния s _i и s ₂ называются бисимулярными (s _i ~ s ₂ ), если существует бисимуляция, содержащая пару (s _i ,s ₂ ). Наибольшее такое отношение — бисимуляционная эквивалентность .

Замечание 1 (Коиндуктивная природа бисимуляции). определение 4 коиндуктивн о4. Бисимуляции суть постнеподвижные точки монотонного функционала уточнения F , где

F(R) = {(s1,s2) | Ф(s1,s2,R)}, а предикат Ф(«1, s2, R) означает, что для пары (si, s2) выполнены условия (i)-(iii) Определения 4 относительно R. Бисимуляционная эквивалентность ~ — наибольшая неподвижная точка vR. F(R), существующая по теореме Кнастера–Тарского ввиду замкнутости множества бисимуляций относительно объединения [6]. Поэтому утверждение si ~ s2 выражает согласованность не одиночного перехода, а всего (вообще говоря, бесконечного) ветвящегося поведения: для каждого конечного или бесконечного пути, исходящего из si, существует зеркальный путь из s2 с попарно бисимулярными состояниями, и наоборот.

Простыми словами: выбор наибольшей неподвижной точки означает презумпцию неотличимости — две реализации считаются эквивалентными до тех пор, пока не предъявлена конкретная последовательность переходов, на которой их поведение расходится. «Различимость» требует свидетеля (такой переход и строит алгоритм 1 при ответе ⊥), тогда как эквивалентность не требует пошаговой проверки всех путей. Именно в этом сила коиндукции: она превращает локальное условие («один переход согласован») в глобальную гарантию («всё бесконечное поведение эквивалентно») — и на этом принципе построены доказательства корректности и полноты настоящей работы (Леммы 1–2), где локальная согласованность переходов через инвариант разбиения распространяется на всё поведение трансдьюсера.

Ключевое свойство бисимуляции: бисимулярные системы удовлетворяют одним и тем же формулам CTL и LTL [6 , теорема 7.14]. Это делает бисимуляцию мощным инструментом верификации: однократная проверка бисимулярности переносит на обе реализации все свойства, выразимые в CTL и LTL, включая заранее не сформулированные, без их поштучной проверки. (Это спецификационно-независимая гарантия эквивалентности поведения, а не обязательно более дешёвая альтернатива проверке одного свойства: выигрыш в стоимости проявляется при переносе многих свойств или при замене системы её бисимулярным, но меньшим представлением.)

Классический алгоритм проверки бисимуляционной эквивалентности [15] основан на методе разбиения (partition refinement) , восходящем к процедуре минимизации детерминированных конечных автоматов (ДКА) Хопкрофта [10] . ДКА — автомат, в котором для каждого состояния и каждого входного символа переход определён однозначно [16] . Алгоритм Хопкрофта строит наименьший (по числу состояний) ДКА, принимающий тот же язык, за время O(n log n), последовательно разбивая состояния на классы эквивалентности. В алгоритме Канеллакиса–Смолки та же идея применяется к двум автоматам одновременно.

Идея. Начинаем с грубого разбиения состояний: все состояния с одинаковой меткой A v (v) в одном блоке. Затем итеративно «дробим» блоки: если два состояния v 1 и v 2 из одного блока имеют переходы по одной метке в разные блоки, они не могут быть бисимулярны и должны быть разделены. Процедура завершается, когда разбиение стабилизируется; итоговые блоки — классы бисимуляционной эквивалентности.

В базовой формулировке алгоритм Канеллакиса–Смолки выполняет O(|V|) проходов уточнения, каждый из которых просматривает все рёбра, и работает за время O(|E| • |V|). Логарифмическая оценка O(|E| • log |V|), совпадающая с оценкой алгоритма Хопкрофта для ДКА, достигается оптимизацией Пейджа–Тарьяна [17]: при разбиении блока на две части в качестве разделителя5 обрабатывается меньшая из них, благодаря чему рёбра каждой вершины участвуют в уточнении не более O(log |V|) раз. Именно эта оптимизированная схема используется в реализации (замечание 7).

3.    GD-бисимуляция: авторское расширение 3.1.    Определение GD-бисимуляции

Стандартная бисимуляция (определение 4) не применима к GD-FST напрямую: метка ребра в GD-FST — это пара (cond, w), а не одиночный символ. Требуется определить, когда два ребра считаются «согласованными».

Авторское нововведение состоит в введении отношения совместимости рёбер, учитывающего как логическую эквивалентность условий охраны, так и совпадение весов. Это расширение нетривиально: проверка логической эквивалентности условий сводится к задаче выполнимости булевых формул или к SMT-проверке для формул с арифметическими ограничениям и6, что принципиально сложнее проверки равенства меток, а совпадение весов требует отдельного обсуждения для стохастических систем. Причина в том, что интерпретация веса различна: для детерминированных атрибутов (урон, стоимость, длительность) точное равенство w 1 = w ₂ не вызывает вопросов, тогда как для вероятностного веса на исходящие из вершины веса наложено ограничение нормировки £_v‘ w(v,v ‘ ) = 1, и сама эквивалентность распадается на точную (равенство вероятностей) и приближённую (ε-близость), задающие разные отношения; этот случай разобран в Замечании 3.

Определение 5 (Совместимость рёбер). Пусть сравниваются два трансдьюсера T 1 и T 2 , и пусть e и e ^′ — рёбра из дизъюнктного объединения E 1 ⊔ E 2 . Для ребра e ∈ E i используется соответствующая функция пометки X E ; то есть X e (e) ниже означает X E (e).

Отношение совместимости задаётся именно на всём объединении E ₁ ⊔ E ₂ , а не только между ребром первого и ребром второго трансдьюсера. В самом определении бисимуляции далее сравниваются переходы из разных состояний, однако алгоритму нужен единый алфавит классов меток для обоих трансдьюсеров. Поэтому на этапе предобработки необходимо уметь помещать в один класс любые два ребра рассматриваемого объединения, в том числе два ребра одного трансдьюсера. Иначе две логически эквивалентные, но синтаксически различные охраны внутри одной модели могли бы попасть в разные классы и сделать проверку излишне строгой.

Рёбра e и e ‘ называются (cond, w)-совместимыми, если:

• ( i )    X E (e) = (cond,w), X E (e ‘ ) = (cond ‘ ,w ‘ );

• ( ii )    cond = cond (логическая эквивалентность условий охраны);

• ( iii )    w = w' (равенство весов).

Обозначение: e ≃ e ^′ .

Замечание 2 (Логическая эквивалентность условий). Условия охраны из Cond рассматриваются как формулы над конечным множеством атомарных предикатов. Если атомарные предикаты трактуются как неделимые булевы переменные, проверка cond ₁ = cond ₂ сводится к проверке невыполнимости формулы — (cond i о cond ₂ ), то есть к задаче SAT (Boolean SATisfiability, выполнимость булевых формул) [18] . Если же атомарные предикаты содержат арифметические ограничения над числовыми переменными (например, timer > 333 или mana > 5), используется SMT-проверка (Satisfiability Modulo Theories) в соответствующей теории [19] . В общем случае SAT-задача NP-полна [18 , 20] . Однако для типичных игровых условий охраны с небольшим числом атомарных предикатов такая проверка обычно не является узким местом, поскольку выполняется однократно на этапе предобработки.

Замечание 3 (Веса и стохастическая эквивалентность). При w G [0,1] и 52v ‘ w(v, v ' ) = 1 (стохастический случай) oпределение 5 iii) задаёт строгое согласование вероятностных весов на уровне отдельных рёбер. Оно близко по духу к вероятностной бисимуляции Ларсена–Скоу [21] , однако не совпадает с её классическим определением: в вероятностной бисимуляции сравниваются суммарные вероятности перехода в классы эквивалентности, а не обязательно веса отдельных рёбер. Поэтому настоящая статья рассматривает точную структурную версию согласования весов. Для ε -приближённой версии (когда допустимо |w ₁ — w ₂ | < е) алгоритм обобщается заменой равенства на ε -близость; полное исследование вероятностного обобщения составляет перспективу будущих работ.

Теперь можно дать центральное определение статьи.

Определение 6 (GD-бисимуляция). Пусть T 1 = (V ₁ , E ₁ ,^X V , ^X E ) и T 2 = (V ₂ , E ₂ , X V , X E ) — два GD-FST трансдьюсера, и пусть в них выделены начальные вершины v ¹ G V ₁ и v 2 G V ₂ . Бинарное отношение R С V ₁ х V ₂ называется GD-бисимуляцией, если для любых (v ₁ ,v ₂ ) G R:

• ( i )    X V (v ₁ ) = X V (v ₂ ) (совпадение наблюдаемых меток вершин);

• ( ii )    для любого ребра e 1 = (v 1 , v 1 ) G E 1 существует ребро e ₂ = (v ₂ , v 2 ) G E 2 такое, что e 1 ~ e ₂ и (v 1 , v 2 ) G R;

• ( iii )    для любого ребра e ₂ = (v ₂ , v 2 ) G E 2 существует ребро e 1 = (v 1 , v 1 ) G E 1 такое, что e 1 ~ e ₂ и (v 1 , v 2 ) G R.

• 3.2.    Свойства GD-бисимуляции

Отмеченные трансдьюсеры (T 1 ,v 0 ) и (T 2 ,v 0 ) называются GD-бисимуляр-ными (T 1 ^ T ₂ ), если существует GD-бисимуляция R такая, что (v 1 ,v 2 ) G R.

Иными словами, два отмеченных трансдьюсера GD-бисимулярны, если любой игровой сценарий, реализуемый в T 1 , может быть воспроизведён в T 2 с теми же наблюдаемыми фазами, совместимыми условиями охраны и совпадающими весами переходов, и наоборот. При этом GD-бисимуляция не требует структурной тождественности трансдьюсеров: допускаются различия в именах вершин, внутренней детализации состояний и способе разбиения поведения на промежуточные шаги, если эти различия не проявляются на уровне выбранной разметки состояний и совместимости переходов. Поэтому речь идёт не об изоморфизме графов, а о поведенческой эквивалентности моделей в заданной наблюдаемой абстракции.

Замечание 4 (Область применимости относительно среды). Поскольку оба трансдьюсера интерпретируются над общим словарём переменных, логическая эквивалентность охран cond 1 ≡ cond 2 означает их срабатывание при тождественных состояниях среды. Поэтому GD-бисимуляция достаточна для эквивалентности управляющего поведения при фиксированной общей интерпретации среды и одинаковой семантике эффектов переходов. Обратное верно лишь относительно выбранного словаря: определение не обнаруживает эквивалентности, для установления которых требуется нетривиальный морфизм между разными словарями переменных.

На языке геймдизайна: если одна реализация измеряет кулдаун в миллисекундах, а другая — в дискретных тиках, их охраны записаны над несопоставимыми атомами и будут признаны несовместимыми, даже когда соответствуют одному физическому интервалу (раздел 6) ; установление такой эквивалентности требует явного отображения сред и составляет открытую задачу.

Детерминизм, недетерминизм и выбор бисимуляции. определение 2 не требует детерминизма: из одной вершины может исходить несколько рёбер, и если их охранные условия одновременно выполнимы, переход недетерминирован. GD-бисимуляция (определение 6) и алгоритм 1 обрабатывают этот случай штатно — условия (ii)-(iii) формулируются через «для каждого ребра существует совместимое», что является стандартной трактовкой ветвящегося недетерминизма [6] и не опирается на единственность перехода. Назовём GD-FST детерминированным в вершине v, если охранные условия исходящих из v рёбер попарно несовместны (их конъюнкция невыполнима), то есть в любом состоянии среды доступен не более чем один переход; корректно построенные механики, как правило, детерминированы в этом смысле.

Выбор бисимуляции , а не более слабой следовой эквивалентности, оправдан с двух сторон: на полностью детерминированных LTS-проекциях следовая эквивалентность и бисимуляция совпадают [6] ; для GD-FST с недетерминированными или перекрывающимися охранами бисимуляция является более строгим отношением и лучше отражает важное для геймдизайнера свойство — какие действия становятся доступны в каждой фазе, а не только в каком порядке они наблюдаются в отдельной партии.

Граничные случаи охран укладываются в ту же схему: cond = Т — безусловный (всегда доступный) переход; cond = 1 — «мёртвое» ребро, которое никогда не срабатывает и удаляется при нормализации входа, что необходимо для совпадения структурного сравнения с семантическим.

Замечание 5 (Наибольшая GD-бисимуляция). Объединение произвольного числа GD-бисимуляций является GD-бисимуляцией. В самом деле, пусть R = [Ji Ri, где каждое R i — GD-бисимуляция, и (v 1 ,v ₂ ) G R. Тогда (v 1 ,v ₂ ) G R j для некоторого j, и условия (i) —(iii) Определения 6 выполнены для этой пары относительно R j ; поскольку они формулируются через существование совместимого ребра с образом в том же отношении, а R j C R, эти образы принадлежат и R — значит, условия выполнены и относительно R . Следовательно, существует наибольшая GD-бисимуляция ~ — отношение GD-бисимуляционной эквивалентности. Это стандартный результат теории бисимуляций [2] , немедленно переносящийся на GD-FST в силу сохранения структуры определения.

Следствие 1 (Сохранение формул темпоральных логик). Пусть 7 1 ^7 2 . Тогда для любой формулы ф темпоральной логики CTL или LTL, атомарные высказывания которой интерпретируются над метками вершин λ V :

7 1 = ф ^^ 7 2 = ф.

Доказательство. Для пары трансдьюсеров T ₁ , T ₂ сначала соберём множество всех меток рёбер обоих трансдьюсеров:

M = {4(e) | e e E 1 } U {A E (e) | e € E 2 },     K = M/ ^ k .

Здесь K — общий алфавит классов совместимых меток, а отношение ≈ K задаётся так:

(cond,w) « _K (cond ‘ ,w ‘ )   ^ z cond = cond ’ Л w = w'.

Из каждого трансдьюсера построим размеченную систему переходов над этим общим алфавитом:

LTSk (Ti) = (Vi,K, ^,AV),     i e {1, 2}, где (v, к, v') € ^i тогда и только тогда, когда (v, v') € Ei и класс метки AE (v, v') равен к.

Факторизация по ≈ K существенна: синтаксически различные метки (cond 1 ,w 1 ) и (cond ₂ ,w ₂ ), связанные отношением « к (логически эквивалентные охраны при равных весах), отождествляются в один символ алфавита K . В полученных таким образом LTS условие совместимости e 1 ≃ e 2 (определение 5) превращается в точное совпадение меток-классов. Следовательно, GD-бисимуляция R (определение 6) есть стандартная бисимуляция между LTS k (7 1 ) и LTS k (7 2 ). Применяя теорему 7.14 из [6] о сохранении формул CTL и LTL при стандартной бисимуляции, получаем T 1 = ф ' z 7 2 = ф. □                                             □

Следствие 1 является ключевым обоснованием практической ценности GD-бисимуляции: если две реализации механики GD-бисимулярны, они не могут быть различены никаким верификационным свойством, выраженным в CTL или LTL. Это означает, что их можно взаимозаменять в любом верификационном пайплайне без изменения результатов проверки.

Замечание 6 (Композициональность — перспектива). Естественным продолжением является вопрос о композициональности: сохраняется ли GD-бисимуляция при параллельной композиции механик, то есть влечёт ли T1 ∼ T1′ и T2 ∼ T2′ эквивалентность композиций T1 ⊗ T2 ∼ T1′ ⊗ T2′. Положительный ответ означал бы возможность модульного рефакторинга: замена отдельной механики на GD-бисимулярную сохраняла бы поведение всей игровой системы. Для классических исчислений процессов конгруэнтность относительно параллельной композиции — известный результат [2], однако его перенос на GD-FST требует предварительной формализации самого оператора композиции для рёбер с составными метками (cond,w), и в первую очередь — фиксации семантики комбинирования весов при синхронизации переходов (произведение вероятностей, сумма стоимостей или иной закон в зависимости от интерпретации веса). Эта формализация и доказательство конгруэнтности составляют предмет отдельного исследования и в настоящей работе не приводятся.

4.    Алгоритм проверки GD-бисимуляции 4.1.    Описание алгоритма

Алгоритм 1 строится по схеме Канеллакиса–Смолки [15] , адаптированной к структуре GD-FST. Адаптация заключается в замене проверки равенства меток рёбер проверкой (cond, w)-совместимости (определение 5) . Это единственное, но принципиальное отличие от классического алгоритма.

Поскольку условия охраны сравниваются по логической эквивалентности (замечание 2) , а не синтаксически, метки рёбер предварительно группируются в классы совместимости . Обозначим отношение эквивалентности на метках рёбер через « K :

(cond,w) ~ K (cond ‘ ,w ‘ ) ^4 cond = cond ’ A w = w .

Дальнейшее уточнение разбиения ведётся по классам K , а не по синтаксическим парам меток. Это устраняет риск развести логически эквивалентные, но синтаксически различные переходы.

Вход : трансдьюсеры 7 1 и T 2 . Выход : Т (бисимулярны) или ± (не бисимулярны), при необходимости — свидетель различия.

В алгоритме 1 через λ V и λ E обозначены объединённые функции разметки на дизъюнктных объединениях V i U V 2 и E 1 U E 2 : на элементах первого трансдьюсера они совпадают с λ ¹ _V , λ ¹ _E , а на элементах второго — с λ ² _V , λ ² _E .

Перед запуском алгоритма 1 предполагается нормализация входных трансдьюсеров: рёбра с невыполнимой охраной cond = ± удаляются, поскольку они не могут быть пройдены ни при каком состоянии среды и не должны влиять на поведенческую эквивалентность.

Алгоритм 1. Проверка GD-бисимуляционной эквивалентности

1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25:

V ← V 1 ⊔ V 2                               ▷ объединение вершин E ← E 1 ⊔ E 2                               ▷ объединение рёбер P 0 ^ {{ v € V : A v (v) = 1 } : I € A v }             > по меткам вершин P 0 ← P 0 \ {∅}                        ▷ исключить пустые блоки M ^ { A E (e) : e € E 1 } U { A E (e) : e € E 2 }               > метки рёбер K ← M/ ≈ K                                ▷ классы меток for all e ∈ E do cls(e) ^ [A E (e)J ~ K                                     > класс ребра end for i ^ 0 repeat P i +1 ← P i for all B ∈ P i и κ ∈ K do Splitter ^ { v € V : 3 e = (v, v ‘ ) € E, cls(e) = к, v ‘ € B } for all C € P i+1 такое, что C П Splitter = 0 и C % Splitter do заменить C на C ∩ Splitter и C \ Splitter end for end for i ^ i + 1 until P i = Pi -1                                   > стабилизация if 3 B € P i : { v j ,v 2 } % B then return ⊤ else return ( ± , Witness )                      > свидетель различия end if

В случае возврата ⊥ алгоритм 1 может дополнительно возвращать свидетель различия

Witness = (C, B, к), где C — блок текущего разбиения, содержащий сравниваемые вершины, B — целевой блок, а κ ∈ K — класс метки перехода, относительно которого блок C был разделён. Формально свидетель задаётся условием

C П SplitterB,K = 0 и C % SplitterB,K, где

Splitter _B,_K = {v € V : 3 e = (v, v ‘ ) € E, cls(e) = к, v ‘ € B}.

Иными словами, в блоке C находятся вершины, одна часть которых имеет переход класса κ в блок B , а другая часть такого перехода не имеет. Поэтому эти вершины не могут оставаться в одном классе бисимуляционной эквивалентности.

Если в результате такого разбиения v ₀ ¹ и v ₀ ² оказываются в разных блоках, то тройка (C, B, к) фиксирует локальную причину неэквивалентности начальных состояний.

Содержательный смысл алгоритма 1. Начинаем с грубого разбиения: все вершины с одинаковой наблюдаемой меткой λ V помещаются в один блок. Затем итеративно уточняем разбиение: если два состояния из одного блока различаются набором достижимых блоков по некоторому классу меток κ ∈ K , они не могут быть GD-бисимулярны — разделяем их. Процедура завершается, когда никакое разделение невозможно. Начальные вершины v ₀ ¹ и v ₀ ² GD-бисимулярны тогда и только тогда, когда они остались в одном блоке.

Недетерминизм обрабатывается корректно и не требует специальной обработки. Если из вершины исходит несколько рёбер одного класса κ в разные целевые блоки, это не мешает алгоритму 1 : при обработке каждого целевого блока B множество Splitter(В,к) содержит ровно те вершины, у которых есть κ-переход именно в B , поэтому две вершины с различающимися наборами достижимых по κ блоков будут разделены на соответствующей итерации. Это отражает определение GD-бисимуляции, требующее для каждого ребра существования совместимого, а не биекции рёбер.

• 4.2.    Вычислительная сложность

Замечание 7 (Сложность Алгоритма 1) . Пусть n = |V 1 | + |V 2 |, m = |E 1 | + |E 2 |, k = |K | — число классов совместимости меток рёбер (Алгоритм 1 , предобработка), k ≤ m . В буквальной реализации псевдокода один проход уточнения рассматривает до |P i | · k ≤ nk разделителей, а вычисление каждого множества Splitter прямым просмотром всех рёбер стоит O(m). Так как число проходов ограничено n (каждый результативный проход увеличивает число блоков, а блоков не более n), наивная верхняя оценка составляет O(k • m • n ² ).

Эта оценка описывает именно прямую реализацию псевдокода, удобную для доказательства корректности. В практической версии используется оптимизация Пейджа–Тарьяна [17] : для каждого класса меток поддерживаются обратные списки предшественников, а при разбиении блока в качестве разделителя обрабатывается меньшая часть. Это снижает стоимость цикла уточнения до O(k • m • log n) в используемой оценке. При фиксированном или малом числе классов меток k такая реализация работает близко к линейно-логарифмической по числу рёбер;

в общем случае зависимость от k остаётся существенной. На практике число различных типов переходов в механике обычно намного меньше числа самих переходов, поэтому проверка остаётся интерактивной для библиотек игровых механик.

Проверки логической эквивалентности охранных условий выполняются однократно на этапе предобработки: метки рёбер кластеризуются по отношению « к (замечание 2) , после чего каждому ребру сопоставляется идентификатор класса совместимости, а проверка e 1 ~ е ₂ сводится к сравнению идентификаторов классов за 0(1). Тем самым стоимость SAT/SMT-проверок вынесена из основного цикла уточнения и не зависит от числа его проходов.

Само построение K требует попарного сравнения меток по отношению « к — O(m 2 ) проверок в худшем случае (или O(m • k) при сравнении лишь с представителями уже образованных классов). Эта стоимость не входит в оценку цикла уточнения: она однократна и на практике мала для охран с небольшим числом атомарных предикатов.

Замечание 8 (Практическая реализация весов и условий охраны). Вещественные веса. Точное равенство w 1 = w ₂ проблематично для вещественных чисел из-за ошибок округления. В реализации платформы Tula веса хранятся как рациональные числа (тип fractions.Fraction языка Python), что обеспечивает точное сравнение. Для ε-приближённой версии (|w 1 — w ₂ | < е) алгоритм обобщается заменой равенства на ε-близость; полная формализация составляет перспективу будущих работ.

Проверка условий охраны. Эквивалентность двух охран проверяется SMT-решателем Z3 [19] : строится формула

— (cond1 о cond2), и проверяется её невыполнимость. Если такая формула невыполнима, то не существует состояния среды, в котором две охраны дают разные истинностные значения. Для типичных игровых условий охраны с небольшим числом атомарных предикатов такая проверка практически не влияет на основной цикл уточнения разбиения.

5.    Корректность и полнота алгоритма

В доказательстве рассматривается дизъюнктное объединение двух трансдьюсеров, как и в алгоритме 1. Поэтому запись v 1 ^ v ₂ в леммах ниже означает принадлежность пары вершин к наибольшей GD-бисимуляции на этом объединении; её ограничение на V 1 х V 2 совпадает с отношением из Определения 6 .

Теорема 1 (Корректность и полнота алгоритма 1) . Алгоритм 1 возвращает ⊤ тогда и только тогда, когда T 1 ∼ T 2 .

Доказательство проводится по классической схеме теории алгоритмов разбиения [6 , 10, 15] . Ниже приводится полное доказательство, адаптированное к структуре GD-FST. Авторский вклад — в установлении того, что адаптация с одиночных меток на классы совместимости рёбер сохраняет все инварианты классического доказательства.

Лемма 1 (Инвариант разбиения). В каждый момент работы Алго ритма 1 выполняется: если v 1 ∼ v 2 , то v 1 и v 2 находятся в одном блоке разбиения P i .

Доказательство по индукции по номеру итерации i.

База. P 0 группирует вершины по λ V -меткам. По условию (i) определе ния 6 v 1 ~ v ₂ влечёт A v (v 1 ) = A v (v ₂ ), т. e. v 1 и v ₂ в одном начальном блоке.

Шаг. Предположим, что инвариант выполнен для P i , и пусть на следующей итерации некоторый блок C ∋ v 1 , v 2 дробится разделителем, построенным по блоку B ∈ P i и классу κ ∈ K . Разделение означает, что одна из вершин имеет переход класса κ в B , а другая нет. Покажем, что для v 1 ~ v ₂ это невозможно. Пусть v 1 имеет ребро e 1 = (v 1 ,v 1 ) с cls(e 1 ) = к и v 1 G B. По условию (ii) определения 6 существует ребро e 2 = (v 2 ,v 2 ) с e 1 — e ₂ (то есть cls(e ₂ ) = к) и v 1 ~ v 2 . По индукционному предположению из v ₁ ^′ ∼ v ₂ ^′ следует, что v ₁ ^′ и v ₂ ^′ лежат в одном блоке P _i ; а поскольку v ₁ ^′ ∈ B и блоки P _i попарно не пересекаются, то v ₂ ^′ ∈ B . Значит, v ₂ также имеет переход класса κ в B. Случай перехода из v ₂ рассматривается симметрично. Поэтому обе вершины одновременно имеют либо не имеют переход класса κ в B и не могут быть разделены данным разделителем. □ □

Лемма 1 означает содержательно: алгоритм никогда не разделяет вершины, которые обязаны быть в одном классе эквивалентности. Это гарантирует корректность (отсутствие ложных отрицаний).

Лемма 2 (Полнота разбиения). Стабилизированное разбиение P ^∗ является наибольшей GD-бисимуляцией, т. е. v ₁ и v ₂ находятся в одном блоке P ^∗ тогда и только тогда, когда v 1 ∼ v 2 .

Доказательство. Обозначим через и отношение «быть в одном блоке» P * . Достаточно показать, что и является GD-бисимуляцией.

Пусть v 1 и v ₂ . Тогда:

• 1.    A v (v 1 ) = A v (v ₂ ): по построению P _o .

• 2.    Пусть e 1 = (v 1 ,v 1 ) — произвольное ребро с cls(e 1 ) = к, и пусть B G P * — блок, содержащий v 1 . Поскольку P * стабильно, разделитель пары (В,к) уже был обработан и не разбил блок, содержащий v 1 и v ₂ ; следовательно, по построению множества Splitter для него обе вершины одновременно либо принадлежат ему, либо нет. Так как v 1 G Splitter (у неё есть переход класса к в B), то и v ₂ G Splitter , то есть существует ребро e ₂ = (v ₂ , v 2 ) с cls(e ₂ ) = к (а значит e 1 ~ e ₂ ) и v 2 G B, откуда v 1 и v 2 .

• 3.    Симметрично.

Таким образом, и — GD-бисимуляция. Поскольку по лемме 1 все GD-бисимулярные пары находятся в одном блоке, и является наибольшей GD-бисимуляцией. □                                        □

Доказательство теоремы 1 . Объединим обе леммы. По определению GD-бисимулярности трансдьюсеров (определение 6) условие 7 1 ^7 2 равносильно v 0 ~ v 2 . Далее, v 0 ~ v 2 выполнено тогда и только тогда, когда v ₀ ¹ и v ₀ ² лежат в одном блоке стабилизированного разбиения P * : импликация «z» обеспечена леммой 1 (бисимулярные вершины никогда не разносятся по разным блокам), а ««» леммой 2 (и есть GD-бисимуляция, поэтому совпадение блоков влечёт бисимулярность). Наконец, заключительная проверка псевдокода возвращает Т в точности тогда, когда v ₀ ¹ и v ₀ ² оказались в одном блоке. Связывая полученные равносильности, имеем

7 1 ^7 2  ^^ v 0 ^ v 2 ,

^^  3B GP * : {v 0 ,v _o ² }С B,

« z алгоритм возвращает Т.

Значит, алгоритм корректен: он возвращает Т ровно для GD-бисимулярных отмеченных трансдьюсеров. □

□

6.    Пример: две реализации механики восстановления способности

Рассмотрим две реализации механики восстановления способности (или кулдауна, от англ. cooldown) — одной из самых распространённых механик в играх с активными способностями, где перезарядка напрямую влияет на баланс. Обе реализации показаны на рисунке 1.

Реализация 7 1 (таймер). Три вершины { v r ,v a ,v c } с фазовыми метками

AV (vR) = READY, AV (vA) = ACTIVE, AV (vc) = COOLDOWN и переходами

A e ( v r ,v a ) = (ready, 1.0),

A E ( v a ,v c ) = (active, 1.0),

A E (v c ,v r ) = (timer > 333, 1.0).

Реализация T 2 (счётчик). Три вершины { u r ,u a ,u c } с фазовыми метками

AV (ur) = READY, AV (uA) = ACTIVE, AV (uc) = COOLDOWN и переходами

A e ( u r ,u a ) = (ready, 1.0),

A E (u A ,u c ) = (active, 1.0),

A E (u c ,u r ) = (ticks > 20, 1.0).

T 1 (таймер)                             .          T 2 (счётчик)

source                                                             source

Рисунок 1. Две реализации механики восстановления способности

Пусть начальные вершины — v 0 = v r и v ^ = u r . Структурно идентичные трансдьюсеры T 1 (таймер) и T 2 (счётчик) совпадают по фазам ( READY , ACTIVE , COOLDOWN ) и по двум переходам, различаясь лишь охранным условием перехода возврата — timer > 333 против ticks > 20.

Вопрос : верно ли, что 7 1 ~ T 2 ?

Применение алгоритма 1 . Начальное разбиение строится по фазовым меткам:

P o = {{ v r ,u r } , { v a ,u a } , {v c ,u c }}.

На первой итерации рассматриваем класс совместимости « timer , содержащий метку (timer > 333, 1.0), и блок B r = { v r ,u r } . У v c есть переход класса K timer в B r , а у и с такого перехода нет: условие ticks > 20 логически не эквивалентно условию timer ≥ 333 над несогласованными словарями переменных. Поэтому блок {v c ,и с } разбивается.

После этого различие распространяется назад. На следующем уточнении разделяются вершины v a и и а , поскольку их переходы по классу (active, 1.0) ведут в уже блоки фазы COOLDOWN . Затем аналогично разделяются начальные вершины v r и u r , так как их переходы по классу (ready, 1.0) ведут в уже разные блоки фазы ACTIVE . Следовательно, алгоритм возвращает ⊥ .

Вывод : T ₁ ̸ ∼ T ₂ . Несмотря на топологическую идентичность, две реализации не эквивалентны по условиям охраны в предположении несогласованных словарей переменных (замечание 4) . Геймдизайнер получает свидетель различия: сначала расходится фаза COOLDOWN , а затем это различие распространяется до начальных вершин фазы READY .

Когда они были бы эквивалентны? Если оба условия определены над согласованными предикатами и логически эквивалентны: timer ≥ 333 ≡ ticks ≥ 20 (например, если задан морфизм среды, согласно которому ticks подсчитывают 16,65 мс-тики, то 20 тиков соответствуют 333 мс). В этом случае алгоритм 1 вернул бы ⊤ , и геймдизайнер получил бы формальное подтверждение поведенческой эквивалентности.

Положительный случай. Рассмотрим успешный рефакторинг над общим словарём предикатов: механика с охраной mana > 5 Л hp > 0 переписана как hp > 0 Л mana > 5 (изменён порядок конъюнктов). Синтаксически метки различны, однако mana > 5 Л hp > 0 = hp > 0 ∧ mana ≥ 5, поэтому на этапе предобработки (SMT-проверка) оба ребра попадают в один класс совместимости, разбиение не дробится, и алгоритм 1 возвращает ⊤ . Этот пример показывает роль предобработки: без факторизации по ≡ наивное посимвольное сравнение меток ошибочно сочло бы две реализации различными.

Неигровой пример: рефакторинг workflow согласования. Ранее упоминалось, что предлагаемый формализм не привязан к играм: те же определения применимы к любой системе, управляемой правилами с охранными условиями и весами. Рассмотрим процесс согласования заявки с фазами DRAFT, REVIEW, APPROVED. В реализации T переход из REVIEW в APPROVED разрешён охраной amount < 1000 Л role = manager, в переработанной реализации Т2 — эквивалентной охраной role = тападегЛ amount ^ 1000 (порядок конъюнктов изменён при рефакторинге). При равных весах переходов метки логически эквивалентны, предобработка помещает их в один класс совместимости, и алгоритм 1 возвращает ⊤: рефакторинг workflow не изменил наблюдаемого поведения. Тем самым проверка бисимуляционной эквивалентности служит инструментом верификации рефакторинга и вне игровой области — всюду, где поведение задаётся размеченными переходами с условиями и весами.

7.    Заключение

В настоящей работе введена GD-бисимуляция — авторское расширение классической бисимуляции Парка–Милнера на GD-FST трансдьюсеры с охранными условиями и числовыми весами (определение 6) . Предложен алгоритм проверки GD-бисимуляционной эквивалентности (алгоритм 1) , построенный на адаптации разбиения Канеллакиса–Смолки [15] . Доказаны корректность и полнота алгоритма (теорема 1) методом индуктивных инвариантов разбиения — стандартной техникой теории алгоритмов эквивалентности [10, 15] . Вычислительная сложность алгоритма в наивной реализации псевдокода составляет O(k • m • n ² ); практическая реализация с оптимизацией Пейджа–Тарьяна [17] снижает стоимость цикла уточнения до O(k • m • log n). Обе оценки полиномиальны по размеру входа.

Работа относится к классу K5 (поведенческая эквивалентность) классификации задач формального анализа игровых механик [11] , решая в его рамках задачу бисимуляционной эквивалентности для моделей GD-FST; другие отношения эквивалентности, минимизация и композициональность в пределах этого класса остаются открытыми (см. ниже).

Полученные результаты опираются на два допущения — общий словарь переменных сравниваемых механик и точное равенство весов; их ослабление составляет содержание перечисленных ниже открытых задач.

Открытыми остаются:

• ( а )    е-приближение : GD-бисимуляция для стохастических механик с близкими (но не равными) вероятностными весами;

• ( б )    временные ограничения : GD-бисимуляция для механик с явным течением времени — переход к временны´ м автоматам и timed-бисимуляции, сохраняющей TCTL [22] ;

• ( в )    минимизация трансдьюсера : факторизация по отношению ~ даёт лишь кандидата на минимальную реализацию и не является непосредственным следствием (см. замечание 9) ;

• ( г )    межсловарная эквивалентность : обнаружение эквивалентности механик, заданных над разными словарями переменных, требующее явного морфизма сред (замечание 4) ;

• ( д )    композициональность: конгруэнтность GD-бисимуляции относительно параллельной композиции механик, требующая предварительной формализации оператора композиции для рёбер с составными метками (замечание 6) .

Замечание 9 (Минимизация как открытая задача). Стабилизированное разбиение P ^∗ (лемма 2) задаёт естественного кандидата на минимальную реализацию — склейку классов GD-бисимулярных вершин. Однако сама факторизация не является непосредственным следствием: при склейке у образа вершины могут возникнуть параллельные рёбра с различными метками (cond,w), тогда как определение 2 допускает не более одной метки на пару вершин. Корректное определение фактор-трансдьюсера поэтому требует закона агрегации параллельных переходов — того же закона комбинирования весов, что и в задаче композициональности (пункт (Д)) , — а также отдельного доказательства минимальности результата.

Направление (а) сводится к замене точного равенства весов на е-близость в отношении совместимости рёбер; направления (б) -(д) требуют расширения формализма — временными ограничениями (б) , законом агрегации весов при склейке и композиции (3, 5) и отображением сред (г).

Алгоритм даёт два непосредственных практических применения:

• ( А ) верификация рефакторинга — доказательство того, что переработанная механика поведенчески тождественна исходной;

( Б ) классификация и сравнение библиотек механик — систематическое сравнение механик из разных игр на эквивалентность в рамках общего словаря переменных, открывающее возможность формального переноса баланса между проектами.

Практическая значимость: алгоритм реализован в платформе Tula [1] и позволяет геймдизайнеру выполнять в интерактивном режиме проверку того, что рефакторинг механики не изменил наблюдаемого поведения. Тот же аппарат применим к любым системам, управляемым правилами с охранными условиями и весами, — сетевым протоколам, рабочим процессам (workflow), мультиагентным системам.