Aller au contenu

Bisimulation

Un article de Wikipédia, l'encyclopédie libre.

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.

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

Logique et bisimulation

[modifier | modifier le code]

Si deux modèles de Kripke sont bisimilaires, alors ils satisfont les mêmes formules de la logique modale. Réciproquement, si de plus les deux modèles de Kripke sont à image finie (tout monde admet au plus un nombre fini de mondes possibles), alors s'ils satisfont les mêmes formules alors ils sont bisimilaires. Ce lien entre bisimulation et logique modale s'appelle le théorème de Henessy-Milner[1].

Van Benthem a démontré que la logique modale est le fragment de la logique du premier ordre qui est invariante par bisimulation[1]. Plus précisément, toute formule du premier ordre invariante par bisimulation est équivalente à la traduction en premier ordre, par la traduction standard, d'une formule de la logique modale. À l'instar du théorème de Van Benthem, Janin et Walukiewicz ont démontré que toute formule de la logique monadique du second ordre invariante par bisimulation est équivalente à une formule du mu-calcul[2].

Références

[modifier | modifier le code]
  1. a et b (en) Patrick Blackburn, Maarten de Rijke et Yde Venema, Modal Logic, Cambridge University Press, (ISBN 978-1-107-05088-4, DOI 10.1017/CBO9781107050884, lire en ligne)
  2. (en) David Janin et Igor Walukiewicz « On the Expressive Completeness of the Propositional Mu-Calculus With Respect to Monadic Second Order Logic » () (lire en ligne, consulté le )
    CONCUR '96: Concurrency Theory
    « (ibid.) », dans Lecture Notes in Computer Science, vol. 1119, Springer
    .