Quelltext der Seite Bisimulation

{{Belege}}
Die [[Theoretische Informatik]] definiert '''Bisimulation''' als [[Relation (Philosophie)|Relation]] zwischen den Zuständen eines [[Transitionssystem]]s, 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.&nbsp;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
:<math>p \longrightarrow^\alpha p',</math>

so gibt es ein q' ∈ S mit
:<math>q \longrightarrow^\alpha q'</math>

und (p',q') ∈ R. Analog gibt es für jedes q' ∈ S mit
:<math>q \longrightarrow^\alpha q'</math>

ein p' ∈ S mit
:<math>p \longrightarrow^\alpha p'</math>

und (p',q') ∈ R.

Äquivalent dazu ist: Sowohl R als auch R<sup>−1</sup> sind Simulations-[[Quasiordnung]]en.

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.
<!-- Note that it is not always the case that if p simulates q and q simulates p then they are bisimilar. For p and q to be bisimilar, the simulation between p and q must be the inverse of the simulation between q and p. -->

== Varianten von Bisimulationen ==

In speziellen Situationen wird der Begriff der Bisimulation manchmal verfeinert, indem weitere Bedingungen hinzugefügt werden. Enthält das Transitionssystem z.&nbsp;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.

{{Normdaten|TYP=s|GND=4619739-4}}

[[Kategorie:Automatentheorie]]