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$⁻¹ 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

Ver também

• Semântica operacional

Referências

1. PARK, David (1981). «Concurrency and Automata on Infinite Sequences». In: Deussen, Peter. Theoretical Computer Science. Proceedings of the 5th GI-Conference, Karlsruhe. Lecture Notes in Computer Science. 104. Springer Science+Business Media. pp. 167–183. ISBN 978-3-540-10576-3. doi:10.1007/BFb0017309 
2. MILNER, Robin (1989). Communication and Concurrency. [S.l.]: Prentice Hall. ISBN 0-13-114984-9 
3. BAIER, Christel; KATOEN, Joost-Pieter. Principles of model checking. [S.l.]: The MIT Press. 20 páginas. ISBN 978-0-262-02649-9  !CS1 manut: Nomes múltiplos: lista de autores (link)
4. HIRSCH, Edward A.; KARHUMÄKI, Juhani; LEPISTÖ, Arto (2012). «Computer Science - Theory and Applications». In: PRILUTSKII, Michail. Computer Science - Theory and Applications. 7th International Computer Science Symposium in Russia, CSR 2012 Nizhny Novgorod, Russia. Springer Science. 191 páginas. ISBN 978-3-642-30641-9  !CS1 manut: Nomes múltiplos: lista de autores (link)
5. SOBOCINSKI, Pawel. «Bisimulation, Games & Hennessy Milner logic» (PDF). Lecture 1 of Modelli Matematici dei Processi Concorrenti. pp. 15–18. Consultado em 5 de março de 2015 
6. VAN BREUGEL, Franck; KASHEFI, Elham; PALAMIDESSI, Catuscia. «A Tribute to Prakash Panangaden». In: RUTTEN, Jan. Horizons of the Mind. Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday. Springer Science. 82 páginas. ISBN 978-3-319-06879-4  !CS1 manut: Nomes múltiplos: lista de autores (link)
7. DRAGOMIR, Alexandru. "Minimal Models and Bisimulation in Modal Logic" . Acessado em 05/03/2015.

Leitura complementar

• Davide Sangiorgi. (2011). Introduction to Bisimulation and Coinduction. Cambridge University Press. ISBN 9781107003637