Bisimulation

aus Wikipedia, der freien Enzyklopädie

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.

[Bearbeiten] 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. Außerdem ist sie die größte Bisimulation über einem gegebenen Transitionssystem.

[Bearbeiten] 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.