Das Kefk Network Wiki befindet sich im Testbetrieb.
Bisimulation
Aus Kefk.
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. Außerdem 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.
 | Dieses Dokument entstammt in seiner ersten oder einer späteren Version der deutschsprachigen Wikipedia. Es ist dort zu finden unter dem Stichwort Bisimulation, die Liste der bisherigen Autoren befindet sich in der Versionsliste; die Originalfassung kann dort auch bearbeitet werden. Alle Texte der Wikipedia und ihre Derivate stehen unter der GNU-Lizenz für freie Dokumentation. |
