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 bisimular, 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
:
so gibt es ein q' ∈ S mit
:
und (p',q') ∈ R. Analog gibt es für jedes q' ∈ S mit
:
ein p' ∈ S mit
:
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 bisimular zu q, geschrieben p ~ q, wenn es eine Bisimulation R mit (p,q) ∈ R gibt.
Die Bisimularitä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.
