Definition

Zustandsübergangssystem S = (Σ, Q, T, i)

(Alphabet Σ, Zustandsmenge Q,
Transitionen T⊆Q×Σ×Q, Startzustand i∈Q)

Relation R⊆Q₁×Q₂ ist Bisimulation zwischen S₁ und S₂, falls:

• Vor- und Nachbereich groß genug: domainR = Q₁, rangeR = Q₂
• Startzustände sind bisimilar: (i₁, i₂)∈R
• S₁-Transitionen durch S₂-Transitionen simuliert:

  ∀(p₁, p₂)∈R : ∀(p₁, a, q₁)∈T₁ :
           ∃q₂ : (p₂, a, q₂)∈T₂∧(q₁, q₂)∈R

• S₂-Transitionen durch S₁-Transitionen simuliert

  Ü: Diagramm zeichnen, Formel hinschreiben