Bisimulation

Dieser Artikel oder nachfolgende Abschnitt ist nicht hinreichend mit Belegen (beispielsweise Einzelnachweisen) ausgestattet. Angaben ohne ausreichenden Beleg könnten demnächst entfernt werden. Bitte hilf Wikipedia, indem du die Angaben recherchierst und gute Belege einfügst.

Die Theoretische Informatik definiert Bisimulation als 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

${\displaystyle p\longrightarrow ^{\alpha }p',}$

so gibt es ein q' ∈ S mit

${\displaystyle q\longrightarrow ^{\alpha }q'}$

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

${\displaystyle q\longrightarrow ^{\alpha }q'}$

ein p' ∈ S mit

${\displaystyle p\longrightarrow ^{\alpha }p'}$

und (p',q') ∈ R.

Äquivalent dazu ist: Sowohl R als auch R⁻¹ 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.