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

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

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

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

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

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

для всех ${\displaystyle p'}$ в ${\displaystyle S}$,

${\displaystyle p{\overset {\alpha }{\rightarrow }}p'}$

подразумевает, что существует ${\displaystyle q'}$ в ${\displaystyle S}$ такой, что

${\displaystyle q{\overset {\alpha }{\rightarrow }}q'}$

и ${\displaystyle (p',q')\in R}$;

и симметрично для всех ${\displaystyle q'}$ в ${\displaystyle S}$

${\displaystyle q{\overset {\alpha }{\rightarrow }}q'}$

подразумевает, что существует ${\displaystyle p'}$ в ${\displaystyle S}$ такой, что

${\displaystyle p{\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)}$ в ${\displaystyle R}$.

Отношение двойственности ${\displaystyle \,\sim \,}$ является отношение эквивалентности. Более того, это наибольшее отношение бимимуляции для данной переходной системы.

Обратите внимание, что не всегда, если ${\displaystyle p}$ имитирует ${\displaystyle q}$ и ${\displaystyle q}$ имитирует ${\displaystyle p}$ тогда они бисимиляры. За ${\displaystyle p}$ и ${\displaystyle q}$ чтобы быть близким, моделирование между ${\displaystyle p}$ и ${\displaystyle q}$ должен быть разговаривать моделирования между ${\displaystyle q}$ и ${\displaystyle p}$. Контрпример (в CCS, описывая кофемашину): ${\displaystyle M=p.{\overline {c}}.M+p.{\overline {t}}.M+p.({\overline {c}}.M+{\overline {t}}.M)}$ и ${\displaystyle M'=p.({\overline {c}}.M'+{\overline {t}}.M')}$ имитируют друг друга, но не являются двойными.

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

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

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

Учитывая маркированная система перехода состояний ${\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}$ к powerset из ${\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 )}$.

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

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

Другой вариант применяется, если система перехода состояний включает понятие тихий (или внутренний) действие, часто обозначаемое ${\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}}}$

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

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

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

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

Алгоритм

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

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

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

использованная литература

1. Байер, Кристель; Катоэн, Йост-Питер (2008). Принципы проверки модели. MIT Press. п. 527. ISBN  978-0-262-02649-9.
2. Байер и Катоэн (2008), Кор. 7.45, стр. 486.

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

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

внешняя ссылка

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

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