Bisimulação - Bisimulation

Na ciência da computação teórica, uma bissimulação é uma relação binária entre sistemas de transição de estado , associando sistemas que se comportam da mesma forma em que um sistema simula o outro e vice-versa.

Intuitivamente, dois sistemas são bissimilares se, presumindo que os vemos como se estivessem jogando um jogo de acordo com algumas regras, correspondam aos movimentos um do outro. Nesse sentido, cada um dos sistemas não pode ser distinguido do outro por um observador.

Definição formal

Dado um sistema de transição de estado marcado ( , , →), onde é um conjunto de estados, é um conjunto de etiquetas e → é um conjunto de transições marcados (ou seja, um subconjunto de ), um bissimulação é uma relação binária , de tal modo que ambos e seu inverso são simulações . Disto segue que o fechamento simétrico de uma bissimulação é uma bissimulação e que cada simulação simétrica é uma bissimulação. Assim, alguns autores definem a bissimulação como uma simulação simétrica. ${\ displaystyle S}$ ${\ displaystyle \ Lambda}$ ${\ displaystyle S}$ ${\ displaystyle \ Lambda}$ ${\ displaystyle S \ times \ Lambda \ times S}$ ${\ displaystyle R \ subseteq S \ times S}$ ${\ displaystyle R}$ ${\ displaystyle R ^ {T}}$

Equivalentemente, é uma bissimulação iff para cada par de estados em e todos os rótulos α em : ${\ displaystyle R}$ ${\ displaystyle (p, q)}$ ${\ displaystyle R}$ ${\ displaystyle \ Lambda}$

se , então existe tal ${\ displaystyle p {\ overset {\ alpha} {\ rightarrow}} p '}$ ${\ displaystyle q {\ overset {\ alpha} {\ rightarrow}} q '}$ ${\ displaystyle (p ', q') \ in R}$ ;

se , então existe tal isso ${\ displaystyle q {\ overset {\ alpha} {\ rightarrow}} q '}$ ${\ displaystyle p {\ overset {\ alpha} {\ rightarrow}} p '}$ ${\ displaystyle (p ', q') \ in R}$ .

Dados dois estados e em , é bisimilar a , escrito , se houver uma bisimulação tal que . Isso significa que a relação de bissimilaridade é a união de todas as bissimulações: exatamente quando para alguma bissimulação . ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle S}$ ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle p \, \ sim \, q}$ ${\ displaystyle R}$ ${\ displaystyle (p, q) \ in R}$ ${\ displaystyle \, \ sim \,}$ ${\ displaystyle (p, q) \ in \, \ sim \,}$ ${\ displaystyle (p, q) \ in R}$ ${\ displaystyle R}$

O conjunto de bissimulações é fechado sob união; portanto, a relação de bissimilaridade é ela própria uma bissimulação. Uma vez que é a união de todas as bissimulações, é a única maior bissimulação. Bisimulações também são fechadas sob fechamento reflexivo, simétrico e transitivo; portanto, a maior bisimulação deve ser reflexiva, simétrica e transitiva. Disto segue que a maior bissimulação - bissimilaridade - é uma relação de equivalência .

Observe que nem sempre é o caso que se simula e simula, então eles são bissimilares. Para e para ser bissimilar, a simulação entre e deve ser o inverso da simulação entre e . Contra-exemplo em CCS : e simulam um ao outro, mas não são bissimilares. ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle q}$ ${\ displaystyle p}$ ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle q}$ ${\ displaystyle p}$ ${\ displaystyle \, M = a.b + a \,}$ ${\ displaystyle \, M '= ab \}$

Definições alternativas

Definição relacional

A bisimulação pode ser definida em termos de composição de relações como segue.

Dado um sistema de transição de estado rotulado , uma relação de bissimulação é uma relação binária sobre (ou seja, ⊆ × ) tal que ${\ displaystyle (S, \ Lambda, \ rightarrow)}$ ${\ displaystyle R}$ ${\ displaystyle S}$ ${\ displaystyle R}$ ${\ displaystyle S}$ ${\ displaystyle S}$ ${\ displaystyle \ forall \ alpha \ in \ Lambda}$

{\ displaystyle R \; \ {\ overset {\ alpha} {\ rightarrow}} \ quad {\ subseteq} \ quad {\ overset {\ alpha} {\ rightarrow}} \; \ R}

e

{\ displaystyle R ^ {- 1} \; \ {\ overset {\ alpha} {\ rightarrow}} \ quad {\ subseteq} \ quad {\ overset {\ alpha} {\ rightarrow}} \; \ R ^ { -1}}

Da monotonicidade e continuidade da composição da relação, segue-se imediatamente que o conjunto das bissimulações é fechado sob uniões (junta-se no poset das relações), e um cálculo algébrico simples mostra que a relação de bissimilaridade - a junção de todas as bissimulações - é uma relação de equivalência. Essa definição e o tratamento associado à bissimilaridade podem ser interpretados em qualquer quantal involutivo .

Definição de ponto fixo

A bissimilaridade também pode ser definida de maneira teórica de ordem , em termos da teoria do ponto fixo, mais precisamente como o maior ponto fixo de uma determinada função definida abaixo.

Dado um sistema de transição de estado rotulado ( , Λ, →), defina como uma função de relações binárias para relações binárias , como segue: ${\ displaystyle S}$ ${\ displaystyle F: {\ mathcal {P}} (S \ times S) \ to {\ mathcal {P}} (S \ times S)}$ ${\ displaystyle S}$ ${\ displaystyle S}$

Seja qualquer relação binária terminada . é definido como o conjunto de todos os pares em ×, de modo que: ${\ displaystyle R}$ ${\ displaystyle S}$ ${\ displaystyle F (R)}$ ${\ displaystyle (p, q)}$ ${\ displaystyle S}$ ${\ displaystyle S}$

{\ displaystyle \ forall \ alpha \ in \ Lambda. \, \ forall p '\ in S. \, p {\ overset {\ alpha} {\ rightarrow}} p' \, \ Rightarrow \, \ exists q '\ em S. \, q {\ overset {\ alpha} {\ rightarrow}} q '\, {\ textrm {e}} \, (p', q ') \ in R}

e

{\ displaystyle \ forall \ alpha \ in \ Lambda. \, \ forall q '\ in S. \, q {\ overset {\ alpha} {\ rightarrow}} q' \, \ Rightarrow \, \ exists p '\ em S. \, p {\ overset {\ alpha} {\ rightarrow}} p '\, {\ textrm {e}} \, (p', q ') \ in R}

A bissimilaridade é então definida como o maior ponto fixo de . ${\ displaystyle F}$

Definição de jogo Ehrenfeucht – Fraïssé

A bisimulaçã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,, de . Ou seja: ${\ displaystyle \ alpha}$ ${\ displaystyle (p, q)}$

${\ displaystyle (p, q) {\ overset {\ alpha} {\ rightarrow}} (p ', q)}$ ou ${\ displaystyle (p, q) {\ overset {\ alpha} {\ rightarrow}} (p, q ')}$

O "Defensor" deve então tentar igualar essa transição, de um ou dependendo do movimento do atacante. Ou seja, eles devem encontrar um tal que: ${\ displaystyle \ alpha}$ ${\ displaystyle (p ', q)}$ ${\ displaystyle (p, q ')}$ ${\ displaystyle \ alpha}$

${\ displaystyle (p ', q) {\ overset {\ alpha} {\ rightarrow}} (p', q ')}$ ou ${\ displaystyle (p, q ') {\ overset {\ alpha} {\ rightarrow}} (p', q ')}$

O atacante e o defensor continuam se alternando até:

O defensor não consegue encontrar nenhuma transição válida para coincidir com o movimento do atacante. Nesse caso, o atacante vence.
O jogo atinge estados que estão ambos 'mortos' (ou seja, não há transições de nenhum dos estados) Neste caso, o defensor vence ${\ displaystyle (p, q)}$
O jogo continua indefinidamente, caso em que o defensor vence.
O jogo chega a estados já visitados. Isso equivale a uma jogada infinita e conta como uma vitória para o defensor. ${\ displaystyle (p, q)}$

Pela definição acima, o sistema é uma bissimulação se e somente se houver uma estratégia de vitória para o defensor.

Definição Coalgebraic

Um bissimulação para sistemas de transição de estado é um caso especial de coalgebraic bissimulação para o tipo de powerset covariante functor . Observe que todo sistema de transição de estado é bijetivamente uma função de para o conjunto de poderes de indexado por escrito como , definido por ${\ displaystyle (S, \ Lambda, \ rightarrow)}$ ${\ displaystyle \ xi _ {\ rightarrow}}$ ${\ displaystyle S}$ ${\ displaystyle S}$ ${\ displaystyle \ Lambda}$ ${\ displaystyle {\ mathcal {P}} (\ Lambda \ times S)}$

{\ displaystyle p \ mapsto \ {(\ alpha, q) \ in \ Lambda \ times S: p {\ overset {\ alpha} {\ rightarrow}} q \}.}

Let ser -ésimo projecção mapeamento a e , respectivamente, para ; e a imagem para frente é definida eliminando o terceiro componente ${\ displaystyle \ pi _ {i} \ dois pontos S \ times S \ a S}$ ${\ displaystyle i}$ ${\ displaystyle (p, q)}$ ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle i = 1,2}$ ${\ displaystyle {\ mathcal {P}} (\ Lambda \ times \ pi _ {1})}$ ${\ displaystyle \ pi _ {1}}$

{\ displaystyle P \ mapsto \ {(\ alpha, p) \ in \ Lambda \ times S: \ existe q. (\ alpha, p, q) \ in P \}}

onde é um subconjunto de . Da mesma forma para . ${\ displaystyle P}$ ${\ displaystyle \ Lambda \ times S \ times S}$ ${\ displaystyle {\ mathcal {P}} (\ Lambda \ times \ pi _ {2})}$

Usando as notações acima, uma relação é uma bissimulação em um sistema de transição se e somente se houver um sistema de transição na relação de modo que o diagrama ${\ displaystyle R \ subseteq S \ times S}$ ${\ displaystyle (S, \ Lambda, \ rightarrow)}$ ${\ displaystyle \ gamma \ colon R \ to {\ mathcal {P}} (\ Lambda \ times R)}$ ${\ displaystyle R}$

comuta, ou seja , para as equações ${\ displaystyle i = 1,2}$

{\ displaystyle \ xi _ {\ rightarrow} \ circ \ pi _ {i} = {\ mathcal {P}} (\ Lambda \ times \ pi _ {i}) \ circ \ gamma}

segure onde está a representação funcional de . ${\ displaystyle \ xi _ {\ rightarrow}}$ ${\ displaystyle (S, \ Lambda, \ rightarrow)}$

Variantes de bisimulação

Em contextos especiais, a noção de bissimulação às vezes é refinada pela adição de requisitos ou restrições adicionais. Um exemplo é o da bissimulação da gagueira , em que uma transição de um sistema pode ser combinada com várias transições do outro, desde que os estados intermediários sejam equivalentes ao estado inicial ("gagueja").

Uma variante diferente se aplica se o sistema de transição de estado inclui uma noção de ação silenciosa (ou interna ), muitas vezes denotada como , ou seja, ações que não são visíveis por observadores externos, então a bissimulação pode ser relaxada para ser uma bissimulação fraca , na qual se dois estados e são bissimilares e há um certo número de ações internas que levam de a algum estado, então deve existir um estado tal que haja algum número (possivelmente zero) de ações internas que levam de a . Uma relação em processos é uma bissimulação fraca se o seguinte for válido (com , e sendo uma transição observável e muda, respectivamente): ${\ displaystyle \ tau}$ ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle p}$ ${\ displaystyle p '}$ ${\ displaystyle q '}$ ${\ displaystyle q}$ ${\ displaystyle q '}$ ${\ displaystyle {\ mathcal {R}}}$ ${\ displaystyle {\ mathcal {S}} \ in \ {{\ mathcal {R}}, {\ mathcal {R}} ^ {- 1} \}}$ ${\ displaystyle a, \ tau}$

${\ displaystyle \ forall p, q. \ quad (p, q) \ in {\ mathcal {S}} \ Rightarrow p {\ stackrel {\ tau} {\ rightarrow}} p '\ Rightarrow \ exists q'. \ quad q {\ stackrel {\ tau ^ {\ ast}} {\ rightarrow}} q '\ wedge (p', q ') \ in {\ mathcal {S}}}$

${\ displaystyle \ forall p, q. \ quad (p, q) \ in {\ mathcal {S}} \ Rightarrow p {\ stackrel {a} {\ rightarrow}} p '\ Rightarrow \ exists q'. \ quad q {\ stackrel {\ tau ^ {\ ast} a \ tau ^ {\ ast}} {\ rightarrow}} q '\ wedge (p', q ') \ in {\ mathcal {S}}}$

Isso está intimamente relacionado à bissimulação até uma relação.

Normalmente, se o sistema de transição de estado fornece a semântica operacional de uma linguagem de programação , então a definição precisa de bissimulação será específica para as restrições da linguagem de programação. Portanto, em geral, pode haver mais de um tipo de relação de bissimulação, (bissimilaridade resp.), Dependendo do contexto.

Bissimulação e lógica modal

Visto que os modelos de Kripke são um caso especial de sistemas de transição de estado (rotulados), a bissimulação também é um tópico na lógica modal . Na verdade, a lógica modal é o fragmento da lógica invariante de primeira ordem sob bisimulação ( teorema de van Benthem ).

Algoritmo

Verificar se dois sistemas de transição finitos são bissimilares pode ser feito em tempo polinomial. Os algoritmos mais rápidos são linear-time usando refinamento de partição por meio de uma redução para o problema de partição mais grosseiro.

Veja também

Referências

Leitura adicional

Park, David (1981). "Concorrência e autômatos em seqüências infinitas". Em Deussen, Peter (ed.). Ciência da Computação Teórica . Proceedings of the 5th GI-Conference, Karlsruhe. Notas de aula em Ciência da Computação . 104 . Springer-Verlag . pp. 167-183. doi : 10.1007 / BFb0017309 . ISBN 978-3-540-10576-3 .
Milner, Robin (1989). Comunicação e simultaneidade . Prentice Hall . ISBN 0-13-114984-9 .
Davide Sangiorgi. (2011). Introdução à Bisimulação e Coindução . Cambridge University Press. ISBN 9781107003637

links externos

Ferramentas de software

CADP : ferramentas para minimizar e comparar sistemas de estados finitos de acordo com várias bissimulações
mCRL2 : ferramentas para minimizar e comparar sistemas de estados finitos de acordo com várias bissimulações
O Jogo do Bisimulation

Languages

In other projects