Бисимуляция

Связь между переходными системами в информатике

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

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

Формальное определение

Учитывая помеченную систему переходов состояний ( , , →), где — набор состояний, — набор меток, а → — набор помеченных переходов (т. е. подмножество ), бисимуляция — это бинарное отношение , такое, что оба и его обратная сторона – симуляции . Отсюда следует, что симметричное замыкание бисимуляции есть бисимуляция и что каждая симметричная симуляция есть бисимуляция. Таким образом, некоторые авторы определяют бисимуляцию как симметричную симуляцию. ^[1] ${\displaystyle S}$ ${\displaystyle \Lambda }$ ${\displaystyle S}$ ${\displaystyle \Lambda }$ ${\displaystyle S\times \Lambda \times S}$ ${\displaystyle R\subseteq S\times S}$ ${\displaystyle R}$ ${\displaystyle R^{T}}$

Эквивалентно, является бисимуляцией тогда и только тогда, когда для каждой пары состояний в и всех меток α в : ${\displaystyle R}$ ${\displaystyle (p,q)}$ ${\displaystyle R}$ ${\displaystyle \Lambda }$

• если , то существует такое, что ${\displaystyle p\mathrel {\overset {\alpha }{\rightarrow }} p'}$ ${\displaystyle q\mathrel {\overset {\alpha }{\rightarrow }} q'}$ ${\displaystyle (p',q')\in R}$ ;
• если , то существует такое, что ${\displaystyle q\mathrel {\overset {\alpha }{\rightarrow }} q'}$ ${\displaystyle p\mathrel {\overset {\alpha }{\rightarrow }} p'}$ ${\displaystyle (p',q')\in R}$ .

Учитывая два состояния и в , является биподобным , записанным тогда и только тогда, когда существует такая бисимуляция, что . Это означает, что отношение биподобия есть объединение всех бисимуляций: именно тогда, когда для некоторой бисимуляции . ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle S}$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle p\,\sim \,q}$ ${\displaystyle R}$ ${\displaystyle (p,q)\in R}$ ${\displaystyle \,\sim \,}$ ${\displaystyle (p,q)\in \,\sim \,}$ ${\displaystyle (p,q)\in R}$ ${\displaystyle R}$

Множество бисимуляций замкнуто по объединению; ^{[Примечание 1]} , следовательно, отношение биподобия само по себе является бисимуляцией. Поскольку это объединение всех бисимуляций, это уникальная и крупнейшая бисимуляция. Бисимуляции также замкнуты при рефлексивном, симметричном и транзитивном замыкании; следовательно, наибольшая бисимуляция должна быть рефлексивной, симметричной и транзитивной. Отсюда следует, что наибольшая бисимуляция — биподобие — является отношением эквивалентности . ^[2]

Альтернативные определения

Реляционное определение

Бисимуляцию можно определить с точки зрения композиции отношений следующим образом.

Учитывая помеченную систему перехода состояний , отношение бисимуляции — это бинарное отношение над (т. е. ⊆ × ), такое что ${\displaystyle (S,\Lambda ,\rightarrow )}$ ${\displaystyle R}$ ${\displaystyle S}$ ${\displaystyle R}$ ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle \forall \alpha \in \Lambda }$

$${\displaystyle R\ ;\ {\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ;\ R}$$

$${\displaystyle R^{-1}\ ;\ {\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ;\ R^{-1}}$$

Из монотонности и непрерывности композиции отношений сразу следует, что множество бисимуляций замкнуто относительно объединений (объединений в ЧУ отношений), а простой алгебраический расчет показывает, что отношение биподобия — объединение всех бисимуляций — есть отношение эквивалентности. Это определение и связанное с ним понимание биподобия можно интерпретировать в любом инволютивном кванте .

Определение фиксированной точки

Биподобие также можно определить теоретико- порядковым способом, с точки зрения теории неподвижной точки , точнее, как наибольшую неподвижную точку определенной функции, определенной ниже.

Для помеченной системы переходов состояний ( , Λ, →) определите функцию от бинарных отношений над к бинарным отношениям над следующим образом: ${\displaystyle S}$ ${\displaystyle F:{\mathcal {P}}(S\times S)\to {\mathcal {P}}(S\times S)}$ ${\displaystyle S}$ ${\displaystyle S}$

Позвольте быть любым бинарным отношением над . определяется как набор всех пар в × таких, что: ${\displaystyle R}$ ${\displaystyle S}$ ${\displaystyle F(R)}$ ${\displaystyle (p,q)}$ ${\displaystyle S}$ ${\displaystyle S}$

$${\displaystyle \forall \alpha \in \Lambda .\,\forall p'\in S.\,p{\overset {\alpha }{\rightarrow }}p'\,\Rightarrow \,\exists q'\in S.\,q{\overset {\alpha }{\rightarrow }}q'\,{\textrm {and}}\,(p',q')\in R}$$

$${\displaystyle \forall \alpha \in \Lambda .\,\forall q'\in S.\,q{\overset {\alpha }{\rightarrow }}q'\,\Rightarrow \,\exists p'\in S.\,p{\overset {\alpha }{\rightarrow }}p'\,{\textrm {and}}\,(p',q')\in R}$$

Тогда биподобие определяется как наибольшая фиксированная точка . ${\displaystyle F}$

Определение игры Эренфойхта – Фрессе.

Бисимуляцию также можно рассматривать как игру между двумя игроками: нападающим и защитником.

«Атакующий» ходит первым и может выбрать любой допустимый переход из . То есть, ${\displaystyle \alpha }$ ${\displaystyle (p,q)}$

$${\displaystyle (p,q){\overset {\alpha }{\rightarrow }}(p',q)}$$

$${\displaystyle (p,q){\overset {\alpha }{\rightarrow }}(p,q')}$$

Затем «Защитник» должен попытаться соответствовать этому переходу, в зависимости от хода атакующего. Т.е. они должны найти такое, что: ${\displaystyle \alpha }$ ${\displaystyle (p',q)}$ ${\displaystyle (p,q')}$ ${\displaystyle \alpha }$

$${\displaystyle (p',q){\overset {\alpha }{\rightarrow }}(p',q')}$$

$${\displaystyle (p,q'){\overset {\alpha }{\rightarrow }}(p',q')}$$

Атакующий и защищающийся продолжают действовать поочередно до тех пор, пока:

• Защитник не может найти никаких допустимых переходов, соответствующих движению атакующего. В этом случае побеждает нападающий.
• Игра достигает состояний , которые оба «мертвы» (т. е. нет переходов ни из одного из состояний). В этом случае защитник выигрывает. ${\displaystyle (p,q)}$
• Игра продолжается вечно, и в этом случае побеждает защитник.
• Игра достигает состояний , которые уже были посещены. Это эквивалентно бесконечной игре и засчитывается как победа защитника. ${\displaystyle (p,q)}$

Согласно приведенному выше определению, система является бисимуляцией тогда и только тогда, когда существует выигрышная стратегия для защищающегося.

Коалгебраическое определение

Бисимуляция для систем с переходом состояний является частным случаем коалгебраической бисимуляции для типа ковариантного функтора степенного множества . Обратите внимание, что каждая система перехода между состояниями является биективной функцией от набора степеней индекса , записанного как , определенного как ${\displaystyle (S,\Lambda ,\rightarrow )}$ ${\displaystyle \xi _{\rightarrow }}$ ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle \Lambda }$ ${\displaystyle {\mathcal {P}}(\Lambda \times S)}$

$${\displaystyle p\mapsto \{(\alpha ,q)\in \Lambda \times S:p{\overset {\alpha }{\rightarrow }}q\}.}$$

Пусть --е проекционное отображение на и соответственно для ; и прямое изображение определяется удалением третьего компонента ${\displaystyle \pi _{i}\colon S\times S\to S}$ ${\displaystyle i}$ ${\displaystyle (p,q)}$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle i=1,2}$ ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{1})}$ ${\displaystyle \pi _{1}}$

$${\displaystyle P\mapsto \{(\alpha ,p)\in \Lambda \times S:\exists q.(\alpha ,p,q)\in P\}}$$

${\displaystyle P}$ ${\displaystyle \Lambda \times S\times S}$ ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{2})}$

Используя приведенные выше обозначения, отношение является бисимуляцией системы переходов тогда и только тогда, когда существует система переходов в отношении такая, что диаграмма ${\displaystyle R\subseteq S\times S}$ ${\displaystyle (S,\Lambda ,\rightarrow )}$ ${\displaystyle \gamma \colon R\to {\mathcal {P}}(\Lambda \times R)}$ ${\displaystyle R}$

коммутирует, т. е. при , уравнения ${\displaystyle i=1,2}$

$${\displaystyle \xi _{\rightarrow }\circ \pi _{i}={\mathcal {P}}(\Lambda \times \pi _{i})\circ \gamma }$$

${\displaystyle \xi _{\rightarrow }}$ ${\displaystyle (S,\Lambda ,\rightarrow )}$

Варианты бисимуляции

В особых контекстах понятие бисимуляции иногда уточняется путем добавления дополнительных требований или ограничений. Примером может служить бисимуляция заикания , в которой один переход одной системы может быть сопоставлен с несколькими переходами другой системы при условии, что промежуточные состояния эквивалентны начальному состоянию («заикания»). ^[3]

Применяется другой вариант, если система перехода состояний включает понятие молчаливого (или внутреннего ) действия, часто обозначаемого , т.е. действия, которые не видны внешним наблюдателям, тогда бисимуляцию можно ослабить до слабой бисимуляции , в которой, если два состояния и биподобны и существует некоторое количество внутренних действий, ведущих из в некоторое состояние , то должно существовать состояние такое, что существует некоторое количество (возможно, ноль) внутренних действий, ведущих из в . Отношение к процессам является слабой бисимуляцией, если выполняется следующее (при этом , и является наблюдаемым и немым переходом соответственно): ${\displaystyle \tau }$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle p}$ ${\displaystyle p'}$ ${\displaystyle q'}$ ${\displaystyle q}$ ${\displaystyle q'}$ ${\displaystyle {\mathcal {R}}}$ ${\displaystyle {\mathcal {S}}\in \{{\mathcal {R}},{\mathcal {R}}^{-1}\}}$ ${\displaystyle a,\tau }$

$${\displaystyle \forall p,q.\quad (p,q)\in {\mathcal {S}}\Rightarrow p{\stackrel {\tau }{\rightarrow }}p'\Rightarrow \exists q'.\quad q{\stackrel {\tau ^{\ast }}{\rightarrow }}q'\wedge (p',q')\in {\mathcal {S}}}$$

$${\displaystyle \forall p,q.\quad (p,q)\in {\mathcal {S}}\Rightarrow p{\stackrel {a}{\rightarrow }}p'\Rightarrow \exists q'.\quad q{\stackrel {\tau ^{\ast }a\tau ^{\ast }}{\rightarrow }}q'\wedge (p',q')\in {\mathcal {S}}}$$

Это тесно связано ^{[ как? ]} к понятию бисимуляции « до » отношения. ^[4]

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

Бисимуляция и модальная логика

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

Алгоритм

Проверка того, что две конечные переходные системы являются биподобными, может быть выполнена за полиномиальное время . ^[5] Самые быстрые алгоритмы являются квазилинейными по времени , используя уточнение разделения путем сведения к самой грубой задаче разделения.

Смотрите также

• Предзаказ моделирования
• Отношение конгруэнтности
• Вероятностное бисимуляция

Примечания

1. Это означает, что объединение двух бисимуляций является бисимуляцией.

Рекомендации

1. Янчар, Петр и Срба, Иржи (2008). «Неразрешимость бисходства принуждением защитника» . Дж. АКМ . Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. 55 (1): 26. дои : 10.1145/1326554.1326559. ISSN  0004-5411. S2CID  14878621.{{cite journal}}: CS1 maint: multiple names: authors list (link)
2. Милнер, Робин (1989). Коммуникация и параллелизм . США: ISBN Prentice-Hall, Inc. 0131149849.
3. Байер, Кристель ; Катоен, Йост-Питер (2008). Принципы проверки моделей . МТИ Пресс. п. 527. ИСБН 978-0-262-02649-9.
4. Дэмиен Поус (2005). «Современные методы слабой бисимуляции». Учеб. 32-й ИКАЛП . Конспекты лекций по информатике . Спрингер Верлаг. 3580 : 730–741.
5. Байер и Катоен (2008), Кор. 7.45, с. 486.

дальнейшее чтение

• Парк, Дэвид (1981). «Параллелизм и автоматы на бесконечных последовательностях». В Деуссене, Питер (ред.). Теоретическая информатика . Материалы 5-й конференции GI, Карлсруэ. Конспекты лекций по информатике . Том. 104. Шпрингер-Верлаг . стр. 167–183. дои : 10.1007/BFb0017309. ISBN 978-3-540-10576-3.
• Милнер, Робин (1989). Коммуникация и параллелизм . Прентис Холл . ISBN 0-13-114984-9.
• Санджорджи, Давиде (2011). Введение в бисимуляцию и коиндукцию. Кембридж, Великобритания: Издательство Кембриджского университета. ISBN 9781107003637. ОСЛК  773040572.

Внешние ссылки

Программные инструменты

• CADP : инструменты для минимизации и сравнения систем с конечными состояниями в соответствии с различными бисимуляциями.
• mCRL2 : инструменты для минимизации и сравнения систем с конечным числом состояний в соответствии с различными бисимуляциями.
• Игра Бисимуляция Игра