¿Cuándo dos simulaciones no son una bisimulación?

20

Dado un sistema de transición etiquetado , donde es un conjunto de estados, es un conjunto de etiquetas y es una relación ternaria. Como de costumbre, escriba para . La transición etiquetada denota que el sistema en estado cambia el estado a con la etiqueta , lo que significa que es una acción observable que causa el cambio de estado.(S,Λ,)SΛ→⊆S×Λ×Spαq(p,α,q)∈→pαqpqαα

Ahora una relación se llama simulación iff RS×S

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

Se dice que un LTS simula otro si existe una relación de simulación entre ellos.

De manera similar, una relación es una bisimulación iffRS×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.

Se dice que dos LTS son bisimilares si existe una bisimulación entre sus espacios de estado.

Claramente, estas dos nociones están bastante relacionadas, pero no son lo mismo.

¿En qué condiciones es el caso de que un LTS simula a otro y viceversa, pero que los dos LTS no son similares?

Dave Clarke
fuente

Respuestas:

12

Debido a que un proceso CCS vale más que mil píxeles, y es fácil ver el LTS subyacente, aquí hay dos procesos que se simulan entre sí, pero no son similares:

P=ab+a
Q=ab

R1={(ab+a,ab),(b,b),(0,b),(0,0)} es una simulación.

R2={(ab,ab+a),(b,b),(0,0)} es una simulación.

P R1 Q y pero y no son bisimilares. Por qué no? Porque y la única tal que es ... y no es bisimilar a .Q R2 PPQPa0QQaQb0b

¿Por qué pueden simularse entre sí, entonces? Porque simula ya que puede hacer todo lo que hace. Y simula porque incluso si puede ir en una -paso a un programa que no hace nada, puede todavía hacer que -paso, y eso es todo lo que se necesita para simular algo. La diferencia clave con la bisimulación es que, como dijo Charles, debe relacionar los mismos procesos con ambas simulaciones. (es decir, tal que tanto como son simulaciones)PQQQPPaQaRRR1

jmad
fuente
10

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).

elección temprana y tardía

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)}rrs2spscpr1pqq , 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).

Gilles 'SO- deja de ser malvado'
fuente
El hecho de que dos simulaciones unidireccionales no sean iguales a la bimilaridad me sugiere que la simulación no es la idea correcta de aproximación en presencia de no determinismo. ¿Hay alguna otra idea que se haya considerado?
Uday Reddy
2

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.LTS1LTS2RLTS2LTS1RR

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).LTS1LTS2RLTS2LTS1R

Charles
fuente
Supongo que lo que estoy tratando de decir es que, en realidad, siempre es el caso de que dos LTS son bimilares, por lo que la pregunta real es más bien si una relación particular es una (bi) simulación.
Charles