En informática teórica una bisimulación es una relación binaria entre sistemas de transición de estados , asociando sistemas que se comportan de la misma forma en que un sistema simula al otro y viceversa.
Intuitivamente, dos sistemas son bisimilares si, asumiendo que los vemos como jugar un juego de acuerdo con algunas reglas, coinciden con los movimientos del otro. En este sentido, cada uno de los sistemas no puede ser distinguido del otro por un observador.
Definicion formal
Dado un sistema de transición de estado etiquetado (, , →), donde es un conjunto de estados, es un conjunto de etiquetas y → es un conjunto de transiciones etiquetadas (es decir, un subconjunto de ), una bisimulación es una relación binaria , tal que ambos y su inverso son simulaciones . De esto se sigue que el cierre simétrico de una bisimulación es una bisimulación, y que cada simulación simétrica es una bisimulación. Así, algunos autores definen la bisimulación como una simulación simétrica. [1]
Equivalentemente, es una bisimulación iff para cada par de estados en y todas las etiquetas α en :
- Si , entonces hay tal que ;
- Si , entonces hay tal que .
Dados dos estados y en , es bisimilar a, escrito , si hay una bisimulación tal que . Esto significa que la relación de bisimilitud es la unión de todas las bisimulaciones: precisamente cuando para alguna bisimulación .
El conjunto de bisimulaciones se cierra bajo unión; [Nota 1] por lo tanto, la relación de bisimilaridad es en sí misma una bisimulación. Dado que es la unión de todas las bisimulaciones, es la única bisimulación más grande. Las bisimulaciones también se cierran bajo cierre reflexivo, simétrico y transitivo; por lo tanto, la bisimulación más grande debe ser reflexiva, simétrica y transitiva. De esto se sigue que la bisimulación más grande, la bisimilaridad, es una relación de equivalencia . [2]
Tenga en cuenta que no siempre es el caso que si simula y simula entonces son bisimilares. Para y para ser bisimilar, la simulación entre y debe ser el inverso de la simulación entre y . Contraejemplo en CCS : y se simulan entre sí pero no son bisimilares.
- ^ Significa que la unión de dos bisimulaciones es una bisimulación.
Definiciones alternativas
Definición relacional
La bisimulación se puede definir en términos de composición de relaciones de la siguiente manera.
Dado un sistema de transición de estado etiquetado , una relación de bisimulación es una relación binaria encima (es decir, ⊆ × ) tal que
- y
De la monotonicidad y continuidad de la composición de relaciones, se sigue inmediatamente que el conjunto de las bisimulaciones está cerrado bajo uniones (se une en el poset de relaciones), y un simple cálculo algebraico muestra que la relación de bisimilaridad —la unión de todas las bisimulaciones— es una relación de equivalencia. Esta definición, y el tratamiento asociado de bisimilarity, pueden interpretarse de cualquier involutivo quantale .
Definición de punto fijo
La bisimilitud también se puede definir en orden teórico , en términos de la teoría del punto fijo, más precisamente como el punto fijo más grande de una determinada función definida a continuación.
Dado un sistema de transición de estado etiquetado (, Λ, →), definir ser una función de relaciones binarias sobre a las relaciones binarias sobre , como sigue:
Dejar ser cualquier relación binaria sobre . se define como el conjunto de todos los pares en × tal que:
y
La bisimilitud se define entonces como el mayor punto fijo de.
Definición del juego Ehrenfeucht – Fraïssé
La bisimulación también se puede pensar en términos de un juego entre dos jugadores: atacante y defensor.
El "atacante" va primero y puede elegir cualquier transición válida, , de . Es decir:
o
El "Defensor" debe intentar igualar esa transición, desde cualquiera o dependiendo del movimiento del atacante. Es decir, deben encontrar un tal que:
o
El atacante y el defensor continúan alternando turnos hasta que:
- El defensor no puede encontrar ninguna transición válida que coincida con el movimiento del atacante. En este caso, el atacante gana.
- El juego llega a estados que están ambos 'muertos' (es decir, no hay transiciones de ninguno de los estados) En este caso, el defensor gana
- El juego continúa para siempre, en cuyo caso gana el defensor.
- El juego llega a estados , que ya han sido visitados. Esto equivale a una jugada infinita y cuenta como una victoria para el defensor.
Según la definición anterior, el sistema es una bisimulación si y solo si existe una estrategia ganadora para el defensor.
Definición coalgebraica
A bisimulación para los sistemas de transición de estados es un caso especial de coalgebraico bisimulación para el tipo de powerset covariante funtor . Tenga en cuenta que cada sistema de transición estatales bijetivamente una función de al grupo de poder de indexado por Escrito como , definido por
Dejar ser -th mapeo de proyección a y respectivamente para ; y la imagen delantera de definido al soltar el tercer componente
dónde es un subconjunto de . Similarmente para.
Usando las notaciones anteriores, una relación es una bisimulación en un sistema de transición si y solo si existe un sistema de transición en la relación tal que el diagrama
conmuta, es decir, para , las ecuaciones
aguantar donde es la representación funcional de .
Variantes de bisimulación
En contextos especiales, la noción de bisimulación a veces se refina agregando requisitos o restricciones adicionales. Un ejemplo es el de la bisimulación de tartamudeo , en el que una transición de un sistema puede coincidir con múltiples transiciones del otro, siempre que los estados intermedios sean equivalentes al estado inicial ("tartamudeos"). [3]
Se aplica una variante diferente si el sistema de transición de estado incluye una noción de acción silenciosa (o interna ), a menudo denotada con, es decir, acciones que no son visibles para los observadores externos, entonces la bisimulación se puede relajar para que sea una bisimulación débil , en la que si dos estados y son bisimilares y hay una serie de acciones internas que a algún estado entonces debe existir el estado de tal manera que hay algún número (posiblemente cero) de acciones internas que a . Una relación en procesos es una bisimulación débil si se cumple lo siguiente (con , y siendo una transición observable y muda respectivamente):
Esto está estrechamente relacionado con la bisimulación hasta una relación.
Normalmente, si el sistema de transición de estado proporciona la semántica operativa de un lenguaje de programación , entonces la definición precisa de bisimulación será específica de las restricciones del lenguaje de programación. Por lo tanto, en general, puede haber más de un tipo de bisimulación, (bisimilaridad o relación) dependiendo del contexto.
Bisimulación y lógica modal
Dado que los modelos de Kripke son un caso especial de sistemas de transición de estado (etiquetados), la bisimulación también es un tema en la lógica modal . De hecho, la lógica modal es el fragmento de la lógica de primer orden invariante bajo bisimulación ( teorema de van Benthem ).
Algoritmo
Se puede comprobar que dos sistemas de transición finitos son bisimilares en tiempo polinomial. [4] Los algoritmos más rápidos son los de tiempo lineal que utilizan el refinamiento de la partición mediante una reducción al problema de partición más burdo.
Ver también
Referencias
- ^ Jančar, Petr y Srba, Jiří (2008). "Indecidibilidad de bisimilaridad por la fuerza del defensor" . J. ACM . Nueva York, NY, EE.UU .: Association for Computing Machinery. 55 (1): 26. doi : 10.1145 / 1326554.1326559 . ISSN 0004-5411 . S2CID 14878621 .CS1 maint: varios nombres: lista de autores ( enlace )
- ^ Milner, Robin (1989). Comunicación y concurrencia . Estados Unidos: Prentice-Hall, Inc. ISBN 0131149849.
- ^ Baier, Christel ; Katoen, Joost-Pieter (2008). Principios de la verificación de modelos . Prensa del MIT. pag. 527. ISBN 978-0-262-02649-9.
- ^ Baier y Katoen (2008) , Cor. 7.45, pág. 486.
Otras lecturas
- Park, David (1981). "Concurrencia y autómatas de secuencias infinitas". En Deussen, Peter (ed.). Informática Teórica . Actas de la 5ª Conferencia GI, Karlsruhe. Apuntes de conferencias en informática . 104 . Springer-Verlag . págs. 167-183. doi : 10.1007 / BFb0017309 . ISBN 978-3-540-10576-3.
- Milner, Robin (1989). Comunicación y concurrencia . Prentice Hall . ISBN 0-13-114984-9.
- Davide Sangiorgi. (2011). Introducción a la bisimulación y la coinducción . Prensa de la Universidad de Cambridge. ISBN 9781107003637
enlaces externos
Herramientas de software
- CADP : herramientas para minimizar y comparar sistemas de estados finitos según diversas bisimulaciones
- mCRL2 : herramientas para minimizar y comparar sistemas de estados finitos según diversas bisimulaciones
- El juego Bisimulation Game