Bisimulation

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 des anderen simulieren kann und umgekehrt.

Anschaulich gesprochen sind zwei Zustände bisimilar, wenn ihre möglichen Züge übereinstimmen. In diesem Sinne können sie von einem außenstehenden Beobachter nicht voneinander unterschieden werden.

Formale Definition

Gegeben sei ein kantenbeschriftetes Transitionssystem (S, Λ, →). Eine Bisimulation ist eine binäre Relation R über S (d.h. R ⊆ S × S) mit:

Für jedes Paar von Zuständen p, q ∈ S gilt: Ist (p,q) ∈ R, so gilt für alle α ∈ Λ: Gibt es ein p' ∈ S mit

p \longrightarrow^\alpha p',

so gibt es ein q' ∈ S mit

q \longrightarrow^\alpha q'

und (p',q') ∈ R. Analog gibt es für jedes q' ∈ S mit

q \longrightarrow^\alpha q'

ein p' ∈ S mit

p \longrightarrow^\alpha p'

und (p',q') ∈ R.

Äquivalent dazu ist: Sowohl R als auch R-1 sind Simulations-Quasiordnungen.

Gegeben zwei Zustände p und q in S, so ist p bisimilar zu q, geschrieben p ~ q, wenn es eine Bisimulation R mit (p,q) ∈ R gibt.

Die Bisimilaritätsrelation ~ ist eine Äquivalenzrelation. Ferner ist sie die größte Bisimulation über einem gegebenen Transitionssystem.

Varianten von Bisimulationen

In speziellen Situationen wird der Begriff der Bisimulation manchmal verfeinert, indem weitere Bedingungen hinzugefügt werden. Enthält das Transitionssystem z.B. einen stillen Übergang, oft gekennzeichnet durch τ, also einen Übergang, der für einen außenstehenden Beobachter nicht sichtbar ist, dann kann die Bisimulation zu einer schwachen Bisimulation abgeschwächt werden, die stille Übergänge ignoriert.


Wikimedia Foundation.

Игры ⚽ Поможем сделать НИР

Schlagen Sie auch in anderen Wörterbüchern nach:

  • 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 — 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… …   Wikipédia en Français

  • 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”