Когда две симуляции не являются бисимуляцией?

20

Для заданной помеченной системы переходов , где - набор состояний, - набор меток, а - троичное отношение. Как обычно, напишите для . Помеченный переход обозначает, что система в состоянии меняет состояние на с меткой , что означает, что - это некоторое наблюдаемое действие, вызывающее изменение состояния.(S,Λ,)SΛ→⊆S×Λ×Spαq(p,α,q)∈→pαqpqαα

Теперь отношение называется имитацией, если RS×S

(p,q)R, if pαp then q,qαq and (p,q)R.

Один LTS считается имитирующим другого, если между ними существует отношение симуляции.

Аналогично, отношение является бисимуляцией, еслиRS×S(p,q)R,

 if pαp then q,qαq and (p,q)R and  if qαq then p,pαp and (p,q)R.

Говорят, что две LTS являются бизоподобными, если между их пространствами состояний существует бисимуляция.

Очевидно, что эти два понятия довольно связаны, но они не совпадают.

При каких условиях LTS имитирует другую, и наоборот, но две LTS не похожи друг на друга?

Дэйв Кларк
источник

Ответы:

12

Поскольку процесс CCS стоит тысячу пикселей - и легко увидеть лежащий в основе LTS - вот два процесса, которые имитируют друг друга, но не похожи друг на друга:

P=ab+a
Q=ab

R1={(ab+a,ab),(b,b),(0,b),(0,0)} является симуляцией.

R2={(ab,ab+a),(b,b),(0,0)} является симуляцией.

P R1 Q и но и не являются бизоподобными. Почему нет? Потому что и единственный такой, что есть ..., а не является бизлоподобным .Q R2 PPQPa0QQaQb0b

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

jmad
источник
10

Даже если в каждом направлении есть моделирование, моделирование назад и вперед может не относиться к одним и тем же наборам состояний. Иногда у вас есть симуляция в одном направлении и симуляция в другом направлении, и два состояния и которые связаны с но не с ни с каким-либо другим моделированием в том же направлении.R1R2p1qR1R2

Канонический пример - две системы, которые имеют одинаковые следы, но делают выбор по- разному. Рассмотрим два автомата для напитков: первый автомат (злой) берет монету ( c) и недетерминированно решает, доставить ли чашку чая ( t). Вторая машина (хорошая) берет монету ( c) и доставляет чашку чая ( t).

ранний и поздний выбор

Хорошая машина имитирует злую машину: возьмите . Все исходящие переходы всех состояний покрыты, включая (который не имеет исходящего перехода, поэтому он тривиален). Обратите внимание, как хорошая машина забывает разницу между и .R1={(s,s),(p,p),(q,q),(r,p)}rrp

Злая машина имитирует хорошую машину: возьмите . Состояние оказывается не используемым в этом моделировании. Фактически, для симуляции невозможно использовать , поскольку должен отображаться в состояние, из которого возможна трасса длины , поэтому это должно быть ; должен отображаться на преемника с меткой , так что это или , но это состояние также должно иметь возможный след длины , поэтому оно должно быть ; и по тем же причинам должен отображаться вR2={(s,s),(p,p),(q,q)}rrs2spscpr1pqq , не оставляя возможности отображения любого состояния в .r

Simuation в одном направлении необходимо отправить где - то. Симуляция в другом направлении должна избегать . Поэтому не существует отношения, которое представляет собой симуляцию в обоих направлениях: системы не являются двойственными.rr

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

Такое различие часто возникает при изучении параллельных систем. Ответ jmad показывает процесс CCS с этим LTS.

Для получения дополнительной информации о бисимуляции я рекомендую заметки Давиде Сангиорги « О происхождении бисимуляции и коиндукции» . (Это упражнение 1 стр. 29, и в примечаниях используется тот же пример.)

Жиль "ТАК - перестань быть злым"
источник
Тот факт, что два однонаправленных моделирования не равны бисходству, наводит меня на мысль, что моделирование не является правильной идеей приближения при наличии недетерминизма. Есть ли другие идеи, которые были рассмотрены?
Uday Reddy
2

Ответ Жиля очень хороший и формальный, и действительно, если моделируется с помощью с отношением , а моделируется с помощью с обратным к , то является бисимуляцией.LTS1LTS2RLTS2LTS1RR

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

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