# Bissimulação

Na teoria da computação uma bissimulação é uma relação binária entre sistemas de transição de estados, ou também chamados apenas de sistemas de transição (sistemas constituintes de estados e transições), associando sistemas que se comportam da mesma maneira no sentido de que um sistema simula o outro e vice-versa.
Intuitivamente dois sistemas são bissimilares se eles combinam seus movimentos entre si. Neste sentido, cada um dos sistemas não pode ser distinto um do outro por um observador.

## Definição formal

Dado um sistema de transição rotulado ($S$, Λ, →); uma relação de bissimulação é uma relação binária $R$ sobre $S$ (isto é, $R$ ⊆ $S$ × $S$) tal que ambos $R$$^{−1}$ e $R$ são simulações.
Equivalentemente $R$ é uma bissimulação se para cada par de elementos $p,q$ em $S$ com $(p,q)$ em $R$, para todo α em Λ:
para todo $p'$ em $S$,
       $p{\overset {\alpha }{\rightarrow }}p'$
    implica que existe um $q'$ em $S$ tal que
       $q{\overset {\alpha }{\rightarrow }}q'$
    e $(p',q')\in R$;
e, simetricamente, para todo $q'$ em $S$
       $q{\overset {\alpha }{\rightarrow }}q'$
    implica que existe um $p'$ em $S$ tal que
       $p{\overset {\alpha }{\rightarrow }}p'$
    e $(p',q')\in R$.
Dados dois estados $p$ e $q$ em $S$, $p$ é bissimilar a $q$, escrito $p\,\sim \,q$, se existe uma bissimulação $R$ tal que $(p,q)$ está em $R$.
A relação de bissimilaridade $\,\sim \,$ é uma relação de equivalência. Além disso, ela é a mais larga relação de bissimulação sobre um dado sistema de transição.
Note que não é sempre o caso que se $p$ simula $q$ e $q$ simula $p$ que eles são bissimilares. Para $p$ e $q$ serem bissimilares, a simulação entre $p$ e $q$ deve ser a inversa da simulação entre $p$ e $q$. Contraexemplo (em Sistemas de Comunicação de Cálculos, descrevendo uma máquina de café): $M=p.{\overline {c}}.M+p.{\overline {t}}.M+p.({\overline {c}}.M+{\overline {t}}.M)$ e $M'=p.({\overline {c}}.M'+{\overline {t}}.M')$ simulam entre si mas não são bissimilares.

## Definições alternativas
### Definição relacional

Bissimulação pode ser definida em termos de composições de relações como segue.
Dado um sistema de transição rotulado $(S,\Lambda ,\rightarrow )$, uma relação de bissimulação é uma relação binária de $R$ sobre $S$ (isto é, $R$ ⊆ $S$ × $S$) tal que $\forall \alpha \in \Lambda$
       $R\ ;\ {\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ;\ R$
    e
       $R^{-1}\ ;\ {\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ;\ R^{-1}$
Partindo da monotonicidade e continuidade da relação de composição, ela segue imediatamente que o conjunto de bissimulações é fechado sobre uniões (junta-se à ordem parcial das relações), e um simples cálculo algébrico mostra que a relação de bissimilaridade - a junção de todas as bissimulações - é uma relação de equivalência. Esta definição, e o tratamento associado a bissimilaridade, pode ser interpretado em qualquer quantale involutivo.

### Definição ponto fixo

Bissimilaridade também pode ser definida da maneira da teoria da ordem, em termos da teoria do ponto fixo, mais precisamente como o maior ponto fixo de uma certa função definida abaixo.
Dado um sistema de transição rotulado ($S$, Λ, →), defina $F:{\mathcal {P}}(S\times S)\to {\mathcal {P}}(S\times S)$ para ser uma função de relações binárias sobre $S$ a relações binárias sobre $S$, como segue:
Seja $R$ uma relação binária qualquer sobre $S$. $F(R)$ é definida para ser o conjunto de todos os pares $(p,q)$ em $S$ × $S$ tal que:
    $\forall \alpha \in \Lambda .\,\forall p'\in S.\,p{\overset {\alpha }{\rightarrow }}p'\,\Rightarrow \,\exists q'\in S.\,q{\overset {\alpha }{\rightarrow }}q'\,{\textrm {e}}\,(p',q')\in R$
e
    $\forall \alpha \in \Lambda .\,\forall q'\in S.\,q{\overset {\alpha }{\rightarrow }}q'\,\Rightarrow \,\exists p'\in S.\,p{\overset {\alpha }{\rightarrow }}p'\,{\textrm {e}}\,(p',q')\in R$
Bissimilaridade então é definida para ser o maior ponto fixo de $F$.

### Definição da teoria dos jogos

Bissimulação também pode ser pensada em termos de um jogo entre dois jogadores, atacante e defensor.
O "Atacante" vai primeiro e pode escolher qualquer transição válida, $\alpha$, de $(p,q)$. Isto é.:
$(p,q){\overset {\alpha }{\rightarrow }}(p',q)$ ou $(p,q){\overset {\alpha }{\rightarrow }}(p,q')$
O "Defensor" deve então tentar combinar aquela transição, $\alpha$ de ambos $(p',q)$ ou $(p,q')$ dependendo do movimento do atacante. Ou seja, eles devem encontrar um $\alpha$ tal que:
$(p',q){\overset {\alpha }{\rightarrow }}(p',q')$ ou $(p,q'){\overset {\alpha }{\rightarrow }}(p',q')$
Atacante e defensor continuam alternando turnos até que:
* O defensor não consegue encontrar uma transição válida para combinar com o movimento do atacante. Neste caso o atacante vence.
* O jogo alcança estados $(p,q)$ que ambos são 'mortos' (ou seja, não há transições de ambos estados). Neste caso o defensor vence.
* O jogo continua para sempre, neste caso o defensor vence.
* O jogo alcança os estados $(p,q)$, que já foram visitados. Isto é o equivalente a um jogo que não termina e conta como vitória para o defensor.
Pela definição acima o sistema é uma bissimulação se e somente se existe uma estratégia de vitória para o defensor.

### Definição co-algébrica

Uma bissimulação do sistema de transição de estados é um caso especial de bissimulação co-algébrica para o tipo de funtor covariante do conjunto das partes. Note que todo o sistema de transições de estados $(S,\Lambda ,\rightarrow )$ é bijetivamente uma função $\xi _{\rightarrow }$ do $S$ para o conjunto das partes de $S$ indexado por $\Lambda$ escrito como ${\mathcal {P}}(\Lambda \times S)$, definido por
       $p\mapsto \{(\alpha ,q)\in S:p{\overset {\alpha }{\rightarrow }}q\}.$
Seja $\pi _{i}\colon S\times S\to S$ o '$i$ ésimo' mapeamento de projeção $(p,q)$ para $p$ e $q$ respectivamente onde $i=1,2$; e ${\mathcal {P}}(\Lambda \times \pi _{1})$ a imagem adiante de $\pi _{1}$ definida por largar o terceiro componente
       $P\mapsto \{(a,p)\in \Lambda \times S:\exists q.(a,p,q)\in P\}$
onde $P$ é um subconjunto de $\Lambda \times S\times S$. Similarmente para ${\mathcal {P}}(\Lambda \times \pi _{2})$.
Usando as notações acima, a relação $R\subseteq S\times S$ é uma bissimulação num sistema de transição $(S,\Lambda ,\rightarrow )$ se e somente se existe um sistema de transição $\gamma \colon R\to {\mathcal {P}}(\Lambda \times R)$ na relação $R$ tal que o diagrama
comuta, isto é para $i=1,2$, as equações
       $\xi _{\rightarrow }\circ \pi _{i}={\mathcal {P}}(\Lambda \times \pi _{i})\circ \gamma$
considerando que $\xi _{\rightarrow }$ é a representação funcional de $(S,\Lambda ,\rightarrow )$.

## Variantes de bissimulação

Em contextos especiais a noção de bissimulação as vezes é refinada pela adição de requisitos adicionais e restrições. Por exemplo se o sistema de transição de estado inclui a noção de ação silenciosa (ou interna), geralmente denotada com $\tau$, isto é ações que não são visíveis por observadores externos, então a bissimulação pode ser descontraída para ser uma bissimulação fraca, a qual se dois estados $p$ e $q$ são bissimilares e existe algum número de ações internas começando por $p$ a outro estado $p'$ então deve existir o estado $q'$ tal que existe algum número (possivelmente zero) de ações internas começando por $q$ a $q'$.
Tipicamente, se o sistema de transição de estado dá a semântica operacional de uma linguagem de programação, então a definição precisa de bissimulação será específica às restrições da linguagem de programação. Portanto, no geral, pode existir mais de um tipo de bissimulação, a relação depende do contexto.

## Bissimulação e lógica modal

Desde que os modelos de Kripke são um caso especial de sistema de transição de estado (rotulado), bissimulação também é um tópico de lógica modal. Na verdade, lógica modal é o fragmento de lógica de primeira ordem invariante sob bissimulação (teorema de Van Benthem).

## Ferramentas de software

* CAPD: para minimizar e comparar sistemas de estados finitos de acordo com várias bissimulações
* O jogo da bissimulação