Bissimulação

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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[1]), 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[editar | editar código-fonte]

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,[2] descrevendo uma máquina de café): e simulam entre si mas não são bissimilares.

Definições alternativas[editar | editar código-fonte]

Definição relacional[editar | editar código-fonte]

Bissimulação pode ser definida em termos de composições de relações[3] 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[editar | editar código-fonte]

Bissimilaridade também pode ser definida da maneira da teoria da ordem, em termos da teoria do ponto fixo,[4] 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[editar | editar código-fonte]

Bissimulação também pode ser pensada em termos de um jogo[5] 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[editar | editar código-fonte]

Uma bissimulação do sistema de transição de estados é um caso especial de bissimulação co-algébrica[6] 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

Coalgebraic bisimulation.svg

comuta, isto é para , as equações

considerando que é a representação funcional de .

Variantes de bissimulação[editar | editar código-fonte]

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[editar | editar código-fonte]

Desde que os modelos de Kripke[7] 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).

Veja também[editar | editar código-fonte]

Ferramentas de software[editar | editar código-fonte]

Referências[editar | editar código-fonte]

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

Leitura complementar[editar | editar código-fonte]

  • Davide Sangiorgi. (2011). Introduction to Bisimulation and Coinduction. Cambridge University Press. ISBN 9781107003637
    • BAIER, Christel;KATOEN, Joost-Pieter. Principles of model checking. [S.l.]: The MIT Press. 20 p.
    • MILNER, Robin. Communication and Concurrency. [S.l.]: Prentice Hall, 1989.
    • HIRSCH, 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.
    • 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
    • SOBOCINSKI, Pawel. Bisimulation, Games & Hennessy Milner logic Lecture 1 of Modelli Matematici dei Processi Concorrenti 15-18 pp.. Visitado em 05/03/2015.
    • VAN 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.
    • DRAGOMIR, Alexandru. "Minimal Models and Bisimulation in Modal Logic". Acessado em 05/03/2015.