Incluso si hay una simulación en cada dirección, las simulaciones de un lado a otro pueden no relacionar los mismos conjuntos de estados. A veces tiene una simulación en una dirección, y una simulación en la otra dirección, y dos estados y que están relacionados por pero no por ni por ninguna otra simulación en la misma dirección.R1R2p1qR1R2
El ejemplo canónico es dos sistemas que tienen los mismos rastros, pero hacen elecciones de manera diferente. Considere dos máquinas de bebidas: la primera máquina (la maligna) toma una moneda ( c
) y decide de manera no determinista si entrega una taza de té ( t
). La segunda máquina (la buena) toma una moneda ( c
) y entrega una taza de té ( t
).
La máquina buena simula la máquina malvada: tome . Todas las transiciones salientes de los estados están cubiertas, incluida (que no tiene transición saliente, por lo que es trivial). Observe cómo la buena máquina olvida la diferencia entre y .R1={(s,s′),(p,p′),(q,q′),(r,p′)}rrp
La máquina malvada simula la máquina buena: tome . El estado no se utiliza en esta simulación. De hecho, no es posible que una simulación use , ya que debe mapearse en un estado desde el cual es posible un rastro de longitud , por lo que debe ser ; debe correlacionarse con un sucesor de con la etiqueta , por lo que es or , pero ese estado también debe tener un posible rastro de longitud , por lo que debe ser ; y por el mismo razonamiento debe correlacionarse conR2={(s′,s),(p′,p),(q′,q)}rrs′2sp′s′cpr1pq′q , sin dejar posibilidad de mapear ningún estado a .r
Una simulación en una dirección debe enviar alguna parte. Una simulación en la otra dirección debe evitar . Por lo tanto, no existe una relación que sea una simulación en ambas direcciones: los sistemas no son bimilares.rr
La diferencia entre las dos máquinas es que la buena máquina es determinista y (suponiendo que viva) siempre entrega té si inserta una moneda, mientras que la máquina malvada puede tomar la moneda por un instante, pero se atasca, incapaz de entregar té.
Este tipo de diferencia surge a menudo en el estudio de sistemas concurrentes. La respuesta de jmad muestra un proceso CCS con este LTS.
Para obtener más información sobre las bisimulaciones, recomiendo las notas de Davide Sangiorgi sobre los orígenes de la bisimulación y la coinducción . (Este es el ejercicio 1 p. 29, y las notas usan el mismo ejemplo).
La respuesta de Gilles es muy buena y formal, y de hecho, si es simulado por con una relación , y es simulado por con el inverso de , entonces es una bisimulación.LTS1 LTS2 R LTS2 LTS1 R R
Sin embargo, si las dos relaciones no son inversas entre sí, entonces es posible que no pueda construir una bisimulación. Por ejemplo, un ejemplo simple proviene del hecho de que la relación vacía es simulación para cualquier LTS. Entonces, podemos tener que es simulado por con una relación , y es simulado por con la relación vacía, y sin embargo, no es necesariamente una bisimulación (aunque tenga en cuenta que la relación vacía también es una bisimulación para cualquier LTS).LTS1 LTS2 R LTS2 LTS1 R
fuente