Relación binaria entre estados de sistemas basados en estados (modelos de Kripke, sistemas de transición etiquetados, procesos) que empareja su comportamiento observable paso a paso: cuando estados relacionados realizan una transición etiquetada a, el estado relacionado puede corresponder con una transición a hacia estados relacionados, y viceversa; la bisimilitud significa que existe tal relación que enlaza los estados.

Principio

Preservar la indiscernibilidad bajo el lenguaje de observación elegido exigiendo un emparejamiento recíproco de transiciones (y de las propiedades de etiquetado), de modo que las propiedades modales e invariantes por bisimulación no distingan estados bisimilares.

Demostración

Dos modelos de Kripke son bisimilares si existe una relación que enlace sus estados iniciales tal que las valoraciones proposicionales coinciden y para cada sucesor en un modelo existe un sucesor emparejado en el otro; las fórmulas modales verdaderas en un estado inicial lo son también en el otro.

Aplicación incorrecta

Usar bisimulación de forma casual como prueba de equivalencia para sistemas con características cuantitativas, probabilísticas, temporales o sensibles a recursos sin adoptar las definiciones correspondientes de bisimulación probabilística o cuantitativa; o concluir isomorfismo a partir de bisimilaridad cuando existen distinciones de ramificación.

Consecuencia

La bisimulación proporciona equivalencia conductual que garantiza la invarianza de las fórmulas modales y muchos lenguajes de especificación; apoya la minimización y cuociente de modelos, el razonamiento por congruencia en cálculos de procesos y técnicas de verificación composicional.

Inversión

Revertir la relación conduce a la simulación: una relación de simulación exige solo un emparejamiento unilateral (un sistema simula a otro) y da lugar a un preorden en lugar de una equivalencia; invertir la perspectiva resalta refinamientos observables más que identidad conductual completa.

Límite

La bisimulación estándar se aplica a sistemas de transición etiquetados y marcos de Kripke con observaciones booleanas; debe adaptarse para sistemas probabilísticos, estocásticos, temporales, híbridos o cuantitativos, y se centra en la estructura de ramificación más que en la equivalencia por trazas lineales.

Tensión semántica

La tensión surge entre bisimulación y equivalencia por trazas: la equivalencia por trazas ignora la ramificación y es más débil, mientras que la bisimulación es más fuerte pero a veces demasiado discriminatoria para especificaciones observacionales; también existe tensión entre bisimulación fuerte y nociones más débiles (branching, weak, observational) que abstraen pasos internos.

Síntesis

La Bisimulación es la relación de emparejamiento recíproco paso a paso que captura la indistinguibilidad conductual en modelos ramificados: al exigir un emparejamiento simétrico de movimientos y observaciones, fundamenta la invariancia modal, la reducción de modelos y el razonamiento composicional, con variantes adaptadas a rasgos cuantitativos de los sistemas.