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çõesBAIER, Christel;KATOEN, Joost-Pieter. Principles of model checking. [S.l.]: The MIT Press. 20 p.), 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 (, Λ, →); uma relação de bissimulação é uma relação binária sobre (isto é, ⊆ × ) tal que ambos −1 e são simulações.

Equivalentemente é uma bissimulação se para cada par de elementos em com em , para todo α em Λ:

para todo em ,

implica que existe um em tal que

e ;

e, simetricamente, para todo em

implica que existe um em tal que

e .

Dados dois estados e em , é bissimilar a , escrito , se existe uma bissimulação tal que está em .

A relação de bissimilaridade é 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 simula e simula que eles são bissimilares. Para e serem bissimilares, a simulação entre e deve ser a inversa da simulação entre e . Contraexemplo (em Sistemas de Comunicação de Cálculos,MILNER, Robin. Communication and Concurrency. [S.l.]: Prentice Hall, 1989. descrevendo uma máquina de café): e 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çõesHIRSCH, Edward A.; KARHUMÄKI, Juhani; LEPISTÖ, Arto (2012). "Computer Science - Theory and Applications" in 7th International Computer Science Symposium in Russia, CSR 2012 Nizhny Novgorod, Russia. PRILUTSKII, Michail Computer Science - Theory and Applications: 191, Springer Science. como segue.

Dado um sistema de transição rotulado , uma relação de bissimulação é uma relação binária de sobre (isto é, ⊆ × ) tal que

e

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,PARK, David (1981). "Concurrency and Automata on Infinite Sequences" in Proceedings of the 5th GI-Conference, Karlsruhe. Deussen, Peter Theoretical Computer Science 104: 167–183 mais precisamente como o maior ponto fixo de uma certa função definida abaixo.

Dado um sistema de transição rotulado (, Λ, →), defina para ser uma função de relações binárias sobre a relações binárias sobre , como segue:

Seja uma relação binária qualquer sobre . é definida para ser o conjunto de todos os pares em × tal que:

e

Bissimilaridade então é definida para ser o maior ponto fixo de .

Definição da teoria dos jogos Bissimulação também pode ser pensada em termos de um jogoSOBOCINSKI, Pawel. Bisimulation, Games & Hennessy Milner logic Lecture 1 of Modelli Matematici dei Processi Concorrenti 15-18 pp.. Visitado em 05/03/2015. entre dois jogadores, atacante e defensor.

O "Atacante" vai primeiro e pode escolher qualquer transição válida, , de . Isto é.:

ou

O "Defensor" deve então tentar combinar aquela transição, de ambos ou dependendo do movimento do atacante. Ou seja, eles devem encontrar um tal que:

ou

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 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 , 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ébricaVAN BREUGEL, Franck; KASHEFI, Elham; PALAMIDESSI, Catuscia. "A Tribute to Prakash Panangaden" in Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday. RUTTEN, Jan Horizons of the Mind: 82, Springer Science. para o tipo de funtor covariante do conjunto das partes. Note que todo o sistema de transições de estados é bijetivamente uma função do para o conjunto das partes de indexado por escrito como , definido por

Seja o ' ésimo' mapeamento de projeção para e respectivamente onde ; e a imagem adiante de definida por largar o terceiro componente

onde é um subconjunto de . Similarmente para .

Usando as notações acima, a relação é uma bissimulação num sistema de transição se e somente se existe um sistema de transição na relação tal que o diagrama

frameless|upright=1.5

comuta, isto é para , as equações

considerando que é a representação funcional de .

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 , 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 e são bissimilares e existe algum número de ações internas começando por a outro estado então deve existir o estado tal que existe algum número (possivelmente zero) de ações internas começando por a .

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 KripkeDRAGOMIR, Alexandru. "Minimal Models and Bisimulation in Modal Logic". Acessado em 05/03/2015. 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

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

Categoria:Ciência da computação teórica Categoria:Métodos formais