В теоретической информатике бисимуляция является бинарным отношением между государственными системами переходной , связывая системы , которые ведут себя так же , как в этой одной системе имитирует другие , и наоборот.
Интуитивно две системы двойственны, если они, если предположить, что мы рассматриваем их как игру по некоторым правилам, соответствуют ходам друг друга. В этом смысле наблюдатель не может отличить каждую из систем от другой.
Формальное определение
Учитывая помеченную систему перехода состояний (, , →), где это набор состояний, - это набор меток, а → - это набор помеченных переходов (т. е. подмножество ), бисимуляция - это бинарное отношение , так что оба и его обратное это моделирование . Из этого следует, что симметричное замыкание бисимуляции является бисимуляцией, и что каждая симметричная симуляция является бисимуляцией. Таким образом, некоторые авторы определяют бисимуляцию как симметричное моделирование. [1]
Эквивалентно, является бисимуляцией тогда и только тогда, когда для каждой пары состояний в и все метки α в :
- если , то есть такой, что ;
- если , то есть такой, что .
Учитывая два состояния а также в , является bisimilar к, написано , если есть бисимуляция такой, что . Это означает, что соотношение бисоподобия это объединение всех бимимуляций: именно когда для некоторой бисимуляции .
Множество бисимуляций замкнуто относительно объединения; [Примечание 1], таким образом, отношение двойного сходства само по себе является бимоделированием. Поскольку это объединение всех бисимуляций, это единственная самая большая бисимуляция. Бисимуляции также замыкаются при рефлексивном, симметричном и транзитивном замыкании; следовательно, самая большая бисимуляция должна быть рефлексивной, симметричной и транзитивной. Отсюда следует, что наибольшая бисимуляция - бисхожесть - является отношением эквивалентности . [2]
Обратите внимание, что не всегда бывает так, что если имитирует а также имитирует тогда они бисимиляры. Для а также чтобы быть близким, моделирование между а также должно быть обратным симуляции между а также . Контрпример в CCS : а также имитируют друг друга, но не являются двойными.
- ^ Это означает, что объединение двух бисимуляций является бисимуляцией.
Альтернативные определения
Реляционное определение
Бисимуляцию можно определить в терминах композиции отношений следующим образом.
Учитывая помеченную систему перехода состояний , отношение бисимуляции - это бинарное отношение над (т.е. ⊆ × ) такой, что
- а также
Из монотонности и непрерывности композиции отношений немедленно следует, что множество бимимуляций замкнуто относительно объединений (объединений в множестве отношений), и простой алгебраический расчет показывает, что отношение биподобия - объединение всех бимимуляций - является отношение эквивалентности. Это определение и связанная с ним трактовка двойного сходства можно интерпретировать с помощью любого инволютивного кванта .
Определение фиксированной точки
Сходство также может быть определено теоретическим способом, с точки зрения теории неподвижных точек, точнее, как наибольшая неподвижная точка определенной функции, определенной ниже.
Учитывая помеченную систему перехода состояний (, Λ, →) определим быть функцией от бинарных отношений над к бинарным отношениям над , следующим образом:
Позволять быть любым бинарным отношением над . определяется как множество всех пар в × такой, что:
а также
Bisimilarity затем определяется как наибольшая фиксированная точка из.
Определение игры Эренфойхта – Фраиссе
Бисимуляцию также можно рассматривать как игру между двумя игроками: нападающим и защитником.
«Атакующий» идет первым и может выбрать любой допустимый переход, , из . Т.е.:
или же
Затем "Защитник" должен попытаться сопоставить этот переход, из любого или же в зависимости от хода нападающего. Т.е. они должны найти такой, что:
или же
Атакующий и защитник продолжают поочередно по очереди, пока:
- Защищающийся не может найти никаких подходящих переходов, соответствующих ходу атакующего. В этом случае выигрывает злоумышленник.
- Игра достигает состояний которые оба «мертвы» (т. е. нет переходов из любого состояния). В этом случае побеждает защитник.
- Игра продолжается вечно, и в этом случае побеждает защитник.
- Игра достигает состояний , которые уже были посещены. Это эквивалентно бесконечной игре и считается победой защитника.
Согласно приведенному выше определению система является бизимуляцией тогда и только тогда, когда существует выигрышная стратегия для защищающегося.
Коалгебраическое определение
Бисимуляция для систем с переходом состояний - это частный случай коалгебраической бисимуляции для типа ковариантного функтора степенного множества . Обратите внимание, что каждая система перехода между состояниямиэто уплотняется функция из к Powerset из проиндексировано написано как , определяется
Позволять быть -я проекционное отображение к а также соответственно для ; а также переднее изображение определяется отбрасыванием третьего компонента
где это подмножество . Аналогично для.
Используя указанные выше обозначения, соотношение является бисимуляцией на переходной системе тогда и только тогда, когда существует переходная система об отношении такая, что диаграмма
ездит на работу, то есть на , уравнения
держись где функциональное представление .
Варианты бисимуляции
В особых контекстах понятие двойного моделирования иногда уточняется путем добавления дополнительных требований или ограничений. Примером может служить бисимуляция заикания , при которой один переход одной системы может быть согласован с несколькими переходами другой, при условии, что промежуточные состояния эквивалентны начальному состоянию («заикания»). [3]
Другой вариант применяется, если система перехода состояний включает понятие молчаливого (или внутреннего ) действия, часто обозначаемого, т. е. действия, которые не видны внешним наблюдателям, то бимимуляцию можно ослабить до слабой бимимуляции , в которой если два состояния а также двойственны, и существует некоторое количество внутренних действий, ведущих из к какому-то состоянию тогда должно существовать состояние такое, что существует некоторое количество (возможно, ноль) внутренних действий, ведущих из к . Отношение на процессах является слабой бимоделированием, если выполняется следующее (с , а также (наблюдаемый и отключенный переходы соответственно):
Это тесно связано с бисимуляцией до отношения.
Как правило, если система перехода между состояниями дает операционную семантику языка программирования , то точное определение бисимуляции будет зависеть от ограничений языка программирования. Поэтому, как правило, может быть более одного вида бисимуляции (соотв. Двойного сходства) в зависимости от контекста.
Бисимуляция и модальная логика
Поскольку модели Крипке являются частным случаем (помеченных) систем с переходами между состояниями, бисимуляция также является темой модальной логики . Фактически модальная логика - это фрагмент логики первого порядка, инвариантный относительно бимимуляции ( теорема ван Бентема ).
Алгоритм
Проверка того, что две конечные переходные системы являются двойными, может быть выполнена за полиномиальное время. [4] Самыми быстрыми алгоритмами являются линейные по времени, использующие уточнение разбиения путем сведения к самой грубой задаче разбиения.
Смотрите также
Рекомендации
- ^ Jančar, Петр и Srba Йиржи (2008). «Неразрешимость двойственности принуждением защитника» . J. ACM . Нью-Йорк, Нью-Йорк, США: Ассоциация вычислительной техники. 55 (1): 26. DOI : 10,1145 / 1326554,1326559 . ISSN 0004-5411 . S2CID 14878621 .CS1 maint: несколько имен: список авторов ( ссылка )
- ^ Милнер, Робин (1989). Коммуникация и параллелизм . США: ISBN Prentice-Hall, Inc. 0131149849.
- ^ Байер, Кристель ; Катоен, Йост-Питер (2008). Принципы проверки модели . MIT Press. п. 527. ISBN 978-0-262-02649-9.
- ^ Байера & Katoen (2008) , Cor. 7.45, стр. 486.
дальнейшее чтение
- Парк, Дэвид (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 : инструменты для минимизации и сравнения систем с конечным числом состояний в соответствии с различными симуляциями
- Игра-симуляция