Bisimulation

Bisimulation

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.

Sommaire

Définition formelle

É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 que à la fois R et R-1 sont des préordres de simulation.

De façon équivalente R est une bisimulation si pour chaque paire 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

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

Références


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Bisimulation de Wikipédia en français (auteurs)

Игры ⚽ Нужно решить контрольную?

Regardez d'autres dictionnaires:

  • Bisimulation — In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice versa.Intuitively two systems are… …   Wikipedia

  • Bisimulation — In der theoretischen Informatik ist eine Bisimulation eine Relation zwischen den Zuständen eines Transitionssystems, die solche Zustände miteinander in Beziehung setzt, die sich gleich verhalten. Das bedeutet, dass der eine Zustand die Übergänge… …   Deutsch Wikipedia

  • bisimulation — noun an equivalence relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice versa See Also: bisimilar, simulation preorder …   Wiktionary

  • Probabilistic bisimulation — is an extension of the concept of bisimulation for fully probabilistic transition systems.A discrete probabilistic transition system is a triple S = (St,Act, au:St imes Act imes St ightarrow [0,1] ) where au(s,a,t) gives the probability of… …   Wikipedia

  • π-calculus — In theoretical computer science, the π calculus (or pi calculus) is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems) …   Wikipedia

  • Pi-calculus — In theoretical computer science, the pi calculus is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems). The aim of the …   Wikipedia

  • Stuttering equivalence — In theoretical computer science, stuttering equivalence, a relation written as:pisim {st}pi , can be seen as a partitioning of path pi and pi into blocks, so that states in the k^{mathrm{th block of one path are labeled (L(sdot)) the same as… …   Wikipedia

  • Semantique de Kripke — Sémantique de Kripke La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à… …   Wikipédia en Français

  • Sémantique de Kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

  • Sémantique de kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”