Bisimulación
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 manera en el sentido de que uno de los sistemas simula al otro y viceversa.
Intuitivamente, dos sistemas son bisimilares si son capaces de imitarse entre sí. En esta perspectiva, un observador no puede distinguir los sistemas entre sí.
Definicion formal
Dado un sistema de transición etiquetado con estados ( S , Λ, →), una relación de bisimulación es una relación binaria R sobre S (es decir, R ⊆ S × S ) tal que tanto R como R −1 son preordenes de simulación .
De manera equivalente, R es una bisimulación si para cada par de elementos p , q en S , si ( p , q ) está en R, entonces para todo α en Λ y para todo p ' en S ,
implica que existe una q ' en S tal que
y ( p ' , q' ) en R , y para todo q ' en S ,
implica que existe una p ' en S tal que
y ( p ' q' ) en R .
Dados dos estados p y q en S , p es bisimilar a q , escrito p ~ q , si hay una bisimulación R tal que ( p , q ) en R .
La relación de bisimilitud ∼ es una relación de equivalencia . Además, es la mayor relación de bisimulación en un sistema de transición dado.
El hecho de que p simule q y q simule p no siempre es suficiente para que sean bisimilares. Para p y q para ser bisimilar, la simulación entre p y q debe ser el inverso de la simulación entre q y p .
Variantes de bisimulación
En contextos particulares, la noción de bisimulación a veces se refina agregando restricciones adicionales. Por ejemplo, si el sistema de transición de estado incluye una noción de acciones silenciosas , a menudo denotadas por τ , es decir, acciones que no son visibles para los observadores externos, entonces la bisimulación puede debilitarse para convertirse en la bisimulación débil , en la que las acciones silenciosas se ignoran.
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 relación bisimulatoria (respectivamente bisimilaridad) dependiendo del contexto.
Lógica y bisimulación
Si dos modelos de Kripke son bisimilares, entonces satisfacen las mismas fórmulas lógicas modales . Por el contrario, si además los dos modelos de Kripke son de imagen finita (cada mundo admite como máximo un número finito de mundos posibles), entonces si satisfacen las mismas fórmulas, entonces son bisimilares. Este vínculo entre la bisimulación y la lógica modal se denomina teorema de Henessy-Milner.
Van Benthem demostró que la lógica modal es el fragmento de la lógica de primer orden que es invariante de bisimulación. Más precisamente, cualquier fórmula de primer orden invariante por bisimulación es equivalente a la traducción de primer orden, por traducción estándar, de una fórmula lógica modal. Siguiendo el ejemplo del teorema de Van Benthem, Janin y Walukiewicz demostraron que cualquier fórmula de lógica monádica de segundo orden invariante por bisimulación es equivalente a una fórmula de cálculo mu .
Ver también
Referencias
- ( fr ) Este artículo está tomado parcial o totalmente del artículo de Wikipedia en inglés titulado " Bisimulation " ( ver la lista de autores ) .
- (en) Patrick Blackburn , Maarten de Rijke y Yde Venema , lógica modal , Cambridge University Press ,2001( ISBN 978-1-107-05088-4 , DOI 10.1017 / CBO9781107050884 , leer en línea )
- (in) David Janin e Igor Walukiewicz (1996) " Sobre la completitud expresiva de la propuesta de cálculo Mu con respecto a la lógica monádica de segundo orden " en CONCUR '96 Notas de la conferencia de teoría de la concurrencia en Ciencias de la computación 1119 , Springer. Consultado el 23 de julio de 2017 .