Bisimulation

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Cet article ne cite pas suffisamment ses sources (février 2013).

Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références » (modifier l'article, comment ajouter mes sources ?).

Ce modèle est-il pertinent ? Cliquez pour voir d'autres.
Cet article ou une de ses sections doit être recyclé. (indiquez la date de pose grâce au paramètre date).

Une réorganisation et une clarification du contenu paraissent nécessaires. Discutez des points à améliorer en page de discussion ou précisez les sections à recycler en utilisant {{section à recycler}}.

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. Une bisimulation sur un même système n'est pas nécessairement une relation d'équivalence, elle n'est même pas nécessairement réflexive.

Intuitivement deux systèmes sont bisimilaires s'ils sont capables de s'imiter l'un l'autre. Dans cette optique, chaque système ne peut être distingué de l'autre par un observateur.

Définition formelle[modifier | modifier le code]

Étant donné un système de transition d'états étiqueté (S, Λ, →), une relation de bisimulation est une relation binaire R sur S (c.à.d 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,

 
p\ \stackrel{\alpha}{\rightarrow}\ p'

implique qu'il existe un q' dans S tel que

 
q\ \stackrel{\alpha}{\rightarrow}\ q'

et (p', q') dans R, et pour tout q' dans S,

 
q\ \stackrel{\alpha}{\rightarrow}\ q'

implique qu'il existe un p' dans S tel que

 
p\ \stackrel{\alpha}{\rightarrow}\ p'

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.

Variantes de la bisimulation[modifier | modifier le code]

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.à.d. 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. Par conséquent, en général, il peut y avoir plus d'une sorte de relation de bisimulation (resp. bisimilarité) en fonction du contexte.

Voir aussi[modifier | modifier le code]

Références[modifier | modifier le code]