Bisimulación

La bisimulación se puede definir en términos de composición de relaciones de la siguiente manera.

Dado un sistema de transición de estados etiquetado${\displaystyle (S,\Lambda ,\rightarrow )}$, una relación de bisimulación es una relación binaria R sobre S (es decir, R ⊆ S × S ) tal que${\displaystyle \forall \lambda \in \Lambda }$

$${\displaystyle R\$$ ;\ {\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\  ;\ R} y $${\displaystyle R^{-1}\$$ ;\ {\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\  ;\ R^{-1}}

De la monotonicidad y continuidad de la composición de relaciones, se deduce inmediatamente que el conjunto de bisimulaciones es cerrado bajo uniones ( uniones en el poset de relaciones), y un cálculo algebraico simple muestra que la relación de bisimilitud —la unión de todas las bisimulaciones— es una relación de equivalencia. Esta definición, y el tratamiento asociado de la bisimilitud, pueden interpretarse en cualquier cuantal involutivo .

La bisimilitud también puede definirse de forma teórica del orden , en términos de la teoría del punto fijo , más precisamente como el mayor punto fijo de una determinada función definida a continuación.

Dado un sistema de transición de estados etiquetado (${\displaystyle S}$, Λ , → ), definir${\displaystyle F:{\mathcal {P}}(S\times S)\to {\mathcal {P}}(S\times S)}$ser una función de relaciones binarias sobre${\displaystyle S}$a relaciones binarias sobre${\displaystyle S}$, de la siguiente manera:

Dejar${\displaystyle R}$cualquier relación binaria sobre${\displaystyle S}$.${\displaystyle F(R)}$se define como el conjunto de todos los pares${\displaystyle (p,q)}$en${\displaystyle S}$×${\displaystyle S}$de tal manera que:

$${\displaystyle \forall \lambda \in \Lambda .\,\forall p'\in S.\,p{\overset {\lambda }{\rightarrow }}p'\,\Rightarrow \,\exists q'\in S.\,q{\overset {\lambda }{\rightarrow }}q'\,{\textrm {y}}\,(p',q')\in R}$$ y $${\displaystyle \forall \lambda \in \Lambda .\,\forall q'\in S.\,q{\overset {\lambda }{\rightarrow }}q'\,\Rightarrow \,\exists p'\in S.\,p{\overset {\lambda }{\rightarrow }}p'\,{\textrm {y}}\,(p',q')\in R}$$

La bisimilitud se define entonces como el mayor punto fijo de${\displaystyle F}$.

La bisimulación también puede pensarse en términos de un juego entre dos jugadores: atacante y defensor. ^{[ 3 ]}

"Atacante" va primero y puede elegir cualquier transición válida,${\displaystyle \lambda }$, de${\displaystyle (p,q)}$. Eso es, $${\displaystyle (p,q){\overset {\lambda }{\rightarrow }}(p',q)}$$ o $${\displaystyle (p,q){\overset {\lambda }{\rightarrow }}(p,q')}$$

El "Defensor" debe entonces intentar igualar esa transición,${\displaystyle \lambda }$de cualquiera de${\displaystyle (p',q)}$o${\displaystyle (p,q')}$dependiendo del movimiento del atacante. Es decir, deben encontrar un ${\displaystyle \lambda }$de tal manera que: $${\displaystyle (p',q){\overset {\lambda }{\rightarrow }}(p',q')}$$ o $${\displaystyle (p,q'){\overset {\lambda }{\rightarrow }}(p',q')}$$

El atacante y el defensor continúan turnándose hasta que:

• El defensor no encuentra ninguna transición válida para igualar el movimiento del atacante. En este caso, el atacante gana.
• El juego llega a los estados${\displaystyle (p,q)}$que ambos están 'muertos' (es decir, no hay transiciones desde ninguno de los dos estados) En este caso, el defensor gana
• El juego se prolonga indefinidamente, en cuyo caso gana el defensor.
• El juego llega a los estados${\displaystyle (p,q)}$, que ya han sido visitadas. Esto equivale a un juego infinito y cuenta como una victoria para el defensor.

Según la definición anterior, el sistema es una bisimulación si y solo si existe una estrategia ganadora para el defensor.

Una bisimulación para sistemas de transición de estado es un caso especial de bisimulación coalgebraica para el tipo de functor de conjunto de potencia covariante . Nótese que cada sistema de transición de estado${\displaystyle (S,\Lambda ,\rightarrow )}$se puede mapear biyectivamente a una función${\displaystyle \xi _{\rightarrow }}$de${\displaystyle S}$al conjunto de potencias de${\displaystyle S}$indexado por${\displaystyle \Lambda }$escrito como${\displaystyle {\mathcal {P}}(\Lambda \times S)}$, definido por $${\displaystyle p\mapsto \{(\lambda ,q)\in \Lambda \times S:p{\overset {\lambda }{\rightarrow }}q\}.}$$

Dejar${\displaystyle \pi _{i}\colon S\times S\to S}$ser${\displaystyle i}$-ésima proyección , mapeo ${\displaystyle (p,q)}$a${\displaystyle p}$y${\displaystyle q}$respectivamente para${\displaystyle i=1,2}$; y ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{1})}$la imagen frontal de${\displaystyle \pi _{1}}$definido por la eliminación del tercer componente $${\displaystyle P\mapsto \{(\lambda ,p)\in \Lambda \times S:\exists q.(\lambda ,p,q)\in P\}}$$ dónde${\displaystyle P}$es un subconjunto de${\displaystyle \Lambda \times S\times S}$. De manera similar para${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{2})}$.

Utilizando las notaciones anteriores, una relación${\displaystyle R\subseteq S\times S}$es una bisimulación en un sistema de transición${\displaystyle (S,\Lambda ,\rightarrow )}$si y solo si existe un sistema de transición${\displaystyle \gamma \colon R\to {\mathcal {P}}(\Lambda \times R)}$sobre la relación${\displaystyle R}$de tal manera que el diagrama

desplazamientos, es decir, para${\displaystyle i=1,2}$, las ecuaciones $${\displaystyle \xi _{\rightarrow }\circ \pi _{i}={\mathcal {P}}(\Lambda \times \pi _{i})\circ \gamma }$$ sostener donde${\displaystyle \xi _{\rightarrow }}$es la representación funcional de${\displaystyle (S,\Lambda ,\rightarrow )}$.

• CADP : herramientas para minimizar y comparar sistemas de estados finitos según diversas bisimulaciones.
• mCRL2 : herramientas para minimizar y comparar sistemas de estados finitos según diversas bisimulaciones.
• El juego de bisimulación