Даже если в каждом направлении есть моделирование, моделирование назад и вперед может не относиться к одним и тем же наборам состояний. Иногда у вас есть симуляция в одном направлении и симуляция в другом направлении, и два состояния и которые связаны с но не с ни с каким-либо другим моделированием в том же направлении.R1R2p1qR1R2
Канонический пример - две системы, которые имеют одинаковые следы, но делают выбор по- разному. Рассмотрим два автомата для напитков: первый автомат (злой) берет монету ( c
) и недетерминированно решает, доставить ли чашку чая ( t
). Вторая машина (хорошая) берет монету ( c
) и доставляет чашку чая ( t
).
Хорошая машина имитирует злую машину: возьмите . Все исходящие переходы всех состояний покрыты, включая (который не имеет исходящего перехода, поэтому он тривиален). Обратите внимание, как хорошая машина забывает разницу между и .R1={(s,s′),(p,p′),(q,q′),(r,p′)}rrp
Злая машина имитирует хорошую машину: возьмите . Состояние оказывается не используемым в этом моделировании. Фактически, для симуляции невозможно использовать , поскольку должен отображаться в состояние, из которого возможна трасса длины , поэтому это должно быть ; должен отображаться на преемника с меткой , так что это или , но это состояние также должно иметь возможный след длины , поэтому оно должно быть ; и по тем же причинам должен отображаться вR2={(s′,s),(p′,p),(q′,q)}rrs′2sp′s′cpr1pq′q , не оставляя возможности отображения любого состояния в .r
Simuation в одном направлении необходимо отправить где - то. Симуляция в другом направлении должна избегать . Поэтому не существует отношения, которое представляет собой симуляцию в обоих направлениях: системы не являются двойственными.rr
Разница между этими двумя машинами заключается в том, что хорошая машина является детерминированной и (при условии живости) всегда доставляет чай, если вы вставляете монету, тогда как злая машина может по прихоти взять монету, но застрянет и не сможет доставить чай.
Такое различие часто возникает при изучении параллельных систем. Ответ jmad показывает процесс CCS с этим LTS.
Для получения дополнительной информации о бисимуляции я рекомендую заметки Давиде Сангиорги « О происхождении бисимуляции и коиндукции» . (Это упражнение 1 стр. 29, и в примечаниях используется тот же пример.)
Ответ Жиля очень хороший и формальный, и действительно, если моделируется с помощью с отношением , а моделируется с помощью с обратным к , то является бисимуляцией.LTS1 LTS2 R LTS2 LTS1 R R
Однако, если эти два отношения не являются обратными друг другу, вы не сможете построить бисимуляцию. Например, простой пример проистекает из того факта, что пустое отношение является симуляцией для любой LTS. Таким образом, мы можем получить , смоделированный с отношением , а , смоделированный с пустым отношением, и все же не обязательно является бисимуляцией (хотя обратите внимание, что пустое отношение также является бисимуляцией для любой LTS).LTS1 LTS2 R LTS2 LTS1 R
источник