Bisimulation

En informatique théorique, une bisimulation est une relation binaire entre des systèmes de transition d'état , associant des systèmes qui se comportent de la même manière dans la mesure où un système simule l'autre et vice versa.

Intuitivement, deux systèmes sont bisimilaires si, en supposant que nous les considérons comme jouant un jeu selon certaines règles, leurs mouvements correspondent. En ce sens, aucun des systèmes ne peut être distingué de l'autre par un observateur.

Étant donné un système de transition d'état étiqueté ( S , Λ, →) , où S est un ensemble d'états, est un ensemble d'étiquettes et → est un ensemble de transitions étiquetées (c'est-à-dire un sous-ensemble de ), une bisimulation est une relation binaire , telle que R et son inverse sont des simulations . Il en résulte que la fermeture symétrique d'une bisimulation est une bisimulation, et que chaque simulation symétrique est une bisimulation. Ainsi, certains auteurs définissent la bisimulation comme une simulation symétrique.

De manière équivalente, R est une bisimulation si et seulement si pour chaque paire d'états dans R et toutes les étiquettes λ dans :

• si , alors il existe un tel que ;
• si , alors il existe tel que .

Étant donné deux états p et q dans S , p est bisimilaire à q , écrit , si et seulement s'il existe une bisimulation R telle que . Cela signifie que la relation de bisimilarité ∼ est l'union de toutes les bisimulations : précisément lorsque pour une certaine bisimulation R .

L'ensemble des bisimulations est fermé par union ; par conséquent, la relation de bisimilarité est elle-même une bisimulation. Puisqu'elle est l'union de toutes les bisimulations, elle est la seule bisimulation la plus grande. Les bisimulations sont également fermées par fermeture réflexive, symétrique et transitive ; par conséquent, la plus grande bisimulation doit être réflexive, symétrique et transitive. Il en résulte que la plus grande bisimulation, la bisimilarité, est une relation d'équivalence .

La bisimulation peut être définie en termes de composition de relations comme suit.

Étant donné un système de transition d'état étiqueté , une relation de bisimulation est une relation binaire R sur S (c'est-à-dire R ⊆ S × S ) telle que

De la monotonie et de la continuité de la composition des relations, il résulte immédiatement que l'ensemble des bisimulations est fermé sous les unions ( jointures dans l' ensemble des relations), et un simple calcul algébrique montre que la relation de bisimilarité – la jointure de toutes les bisimulations – est une relation d'équivalence. Cette définition, et le traitement associé de la bisimilarité, peuvent être interprétés dans n'importe quel quantale involutif .

La bisimilarité peut également être définie de manière théorique , en termes de théorie du point fixe , plus précisément comme le plus grand point fixe d'une certaine fonction définie ci-dessous.

Étant donné un système de transition d'état étiqueté ( , Λ, →), définissons comme une fonction de relations binaires sur vers des relations binaires sur , comme suit :

Soit une relation binaire quelconque sur . est définie comme étant l'ensemble de toutes les paires de × telles que :

La bisimilarité est alors définie comme le plus grand point fixe de .

La bisimulation peut également être pensée en termes de jeu entre deux joueurs : l'attaquant et le défenseur.

L'« attaquant » commence et peut choisir n'importe quelle transition valide, , à partir de . C'est-à-dire, ou

Le « Défenseur » doit alors tenter de faire correspondre cette transition, soit à partir de ou selon le mouvement de l'attaquant. C'est-à-dire qu'il doit trouver un tel que : ou

L'attaquant et le défenseur continuent à alterner jusqu'à ce que :

• Le défenseur ne parvient pas à trouver de transitions valables pour correspondre au mouvement de l'attaquant. Dans ce cas, l'attaquant gagne.
• Le jeu atteint des états qui sont tous deux « morts » (c'est-à-dire qu'il n'y a aucune transition depuis l'un ou l'autre état). Dans ce cas, le défenseur gagne
• Le jeu continue indéfiniment, auquel cas le défenseur gagne.
• Le jeu atteint les états , qui ont déjà été visités. Cela équivaut à une partie infinie et compte comme une victoire pour le défenseur.

Selon la définition ci-dessus, le système est une bisimulation si et seulement s'il existe une stratégie gagnante pour le défenseur.

Une bisimulation pour les systèmes de transition d'état est un cas particulier de bisimulation coalgébrique pour le type de foncteur d'ensemble de puissance covariant . Notez que tout système de transition d'état peut être mappé bijectivement à une fonction de à l' ensemble de puissance de indexé par écrit comme , défini par

Soit la -ième projection , mappée sur et respectivement pour ; et l'image directe de définie en supprimant le troisième composant où est un sous - ensemble de . De même pour .

En utilisant les notations ci-dessus, une relation est une bisimulation sur un système de transition si et seulement s'il existe un système de transition sur la relation tel que le diagramme

commute, c'est-à-dire que pour , les équations sont vraies où est la représentation fonctionnelle de .

Dans des contextes particuliers, la notion de bisimulation est parfois affinée en ajoutant des exigences ou des contraintes supplémentaires. Un exemple est celui de la bisimulation par bégaiement , dans laquelle une transition d'un système peut être mise en correspondance avec plusieurs transitions de l'autre, à condition que les états intermédiaires soient équivalents à l'état de départ (« bégaiements »).

Une variante différente s'applique si le système de transition d'état inclut une notion d' action silencieuse (ou interne ), souvent désignée par , c'est-à-dire des actions qui ne sont pas visibles par des observateurs externes, alors la bisimulation peut être assouplie pour être une bisimulation faible , dans laquelle si deux états et sont bisimilaires et qu'il existe un certain nombre d'actions internes menant de à un certain état, alors il doit exister un état tel qu'il existe un certain nombre (éventuellement zéro) d'actions internes menant de à . Une relation sur les processus est une bisimulation faible si ce qui suit est vrai (avec , et étant respectivement une transition observable et muette) :

Ceci est étroitement lié à la notion de bisimulation « jusqu'à » une relation.

En règle générale, si le système de transition d'état donne la sémantique opérationnelle d'un langage de programmation , 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'un type de relation de bisimulation (respectivement de bisimilarité) selon le contexte.

Les modèles de Kripke étant un cas particulier de systèmes de transition d'état (étiquetés), la bisimulation est également un sujet de la logique modale . En fait, la logique modale est le fragment de la logique du premier ordre invariant sous bisimulation ( théorème de van Benthem ).

La vérification que deux systèmes de transition finis sont bisimilaires peut être effectuée en temps polynomial . Les algorithmes les plus rapides sont en temps quasi-linéaire utilisant un raffinement de partition via une réduction au problème de partition le plus grossier.