Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Bisimulation
Résumé
En informatique théorique, une bisimulation est une relation binaire entre systèmes de transition d'états, associant les systèmes qui se comportent de la même façon au sens qu'un des systèmes simule l'autre et vice-versa.
Intuitivement, deux systèmes sont bisimilaires s'ils sont capables de s'imiter l'un l'autre. Dans cette optique, les systèmes ne peuvent être distingués l'un de l'autre par un observateur.
Étant donné un système de transition d'états étiqueté (S, Λ, →), une relation de bisimulation est une relation binaire R sur S (c'est-à-dire R ⊆ S × S) telle qu'à la fois R et R−1 sont des préordres de simulation.
De façon équivalente R est une bisimulation si pour chaque couple d'éléments p, q dans S, si (p, q) est dans R alors pour tout α dans Λ, et pour tout p''' dans S,
implique qu'il existe un q dans S tel que
et (p' , q' ) dans R, et pour tout q''' dans S,
implique qu'il existe un p dans S tel que
et (p' , q' ) dans R.
Étant donnés deux états p et q dans S, p est bisimilaire à q, noté p ∼ q, s'il existe une bisimulation R telle que (p, q) soit dans R.
La relation de bisimilarité ∼ est une relation d'équivalence. De plus, c'est la plus grande relation de bisimulation sur un système de transition donné.
Le fait que p simule q et q simule p ne suffit pas toujours pour qu'ils soient bisimilaires. Pour que p et q soient bisimilaires, la simulation entre p et q doit être l'inverse de la simulation entre q et p.
Dans des contextes particuliers la notion de bisimulation est parfois raffinée en ajoutant des contraintes supplémentaires. Par exemple si le système de transition d'états inclut une notion d'actions silencieuses, souvent dénotées par τ, c'est-à-dire des actions qui ne sont pas visibles par les observateurs externes, alors la bisimulation peut être affaiblie pour devenir la bisimulation faible, dans laquelle les actions silencieuses sont ignorées.
Typiquement, si le système de transition d'états donne la sémantique opérationnelle d'un langage de programmation, alors la définition précise de la bisimulation sera spécifique aux restrictions du langage de programmation.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.