Бисимуляция - Bisimulation

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

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

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

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

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

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

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

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

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

Обратите внимание, что это не всегда так, что если имитирует и моделирует, то они двойственны. Для и быть bisimilar, моделирование между и должно быть обратное симуляции между и . Контрпример в CCS : и имитируют друг друга, но не являются двойными. ${\ displaystyle p}$${\ displaystyle q}$${\ displaystyle q}$${\ displaystyle p}$${\ displaystyle p}$${\ displaystyle q}$${\ displaystyle p}$${\ displaystyle q}$${\ displaystyle q}$${\ displaystyle p}$${\ Displaystyle \, М = а.б + а \,}$${\ Displaystyle \, М '= ab \}$

---

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

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

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

Учитывая меченого состояние системы перехода , A бисимуляция соотношение представляет собой бинарное отношение над (т.е. ⊆ × ) таким образом, что ${\ 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 {\ substeq} \ quad {\ overset {\ alpha} {\ rightarrow}} \; \ R}$

а также

${\ Displaystyle R ^ {- 1} \; \ {\ overset {\ alpha} {\ rightarrow}} \ quad {\ substeq} \ 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 '\ в 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 '\ в S. \, p {\ overset {\ alpha} {\ rightarrow}} p '\, {\ textrm {and}} \, (p', q ') \ in R}$

Bisimilarity затем определяется как наибольшая фиксированная точка из . ${\ 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 (п ', д)}$${\ 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)}$

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

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

Бисимуляция для систем с переходом состояний - это частный случай коалгебраической бисимуляции для типа ковариантного функтора степенного множества . Следует отметить , что любая система перехода состояния является взаимно однозначно зависит от к Powerset из индексируется записывается в виде , определяется ${\ 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 \}.}$

Пусть be -я проекция отображается в и соответственно для ; и прямое изображение определяется путем отбрасывания третьего компонента ${\ displaystyle \ pi _ {i} \ двоеточие 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: \ существует q. (\ alpha, p, q) \ in P \}}$

где есть подмножество . Аналогично для . ${\ displaystyle P}$${\ displaystyle \ Lambda \ times S \ times S}$${\ Displaystyle {\ mathcal {P}} (\ Lambda \ times \ pi _ {2})}$

Используя указанные выше обозначения, отношение является бимоделированием системы переходов тогда и только тогда, когда существует система переходов на отношении такая, что диаграмма${\ Displaystyle R \ substeq S \ times S}$${\ displaystyle (S, \ Lambda, \ rightarrow)}$${\ Displaystyle \ gamma \ двоеточие 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)}$

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

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

Другой вариант применяется, если система перехода состояний включает в себя понятие тихого (или внутреннего ) действия, часто обозначаемого значком , т. Е. Действий, которые не видны внешними наблюдателями, тогда бисимуляция может быть ослаблена до слабой бисимуляции , в которой если два состояния и являются двойными, и существует некоторое количество внутренних действий, ведущих от к некоторому состоянию, тогда должно существовать такое состояние , что существует некоторое количество (возможно, ноль) внутренних действий, ведущих от к . Отношение процессов является слабой бимоделированием, если выполняется следующее (с , и является наблюдаемым и немым переходом соответственно): ${\ Displaystyle \ тау}$${\ 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 а, \ тау}$

${\ 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}}}$

Это тесно связано с бисимуляцией до отношения.

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

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

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

Алгоритм

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

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

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

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

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

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

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

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

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