Bestimmung einer Bisimulation (Plan)

• Eingabe: Systeme (S₁, S₂)
• berechne Folge von Relationen R₀, R₁…⊆Q₁×Q₂

  wobei (p₁, p₂)∈R_k p₁ in S₁ und p₂ in S₂ verhalten sich für Transitionsfolgen der Länge ≤k „gleich``

• Folge ist monoton fallend bzgl. Inklusion: Q₁×Q₂ = R₀⊇R₁⊇R₂⊇…
• falls diese Folge schließlich stationär ist ( ∃n : R_n = R_n+1), dann teste, ob dieses R_n eine Bisimulation für (S₁, S₂) ist.

Sätze: Korrektheit, Vollständigkeit,

Termination für endliche Q₁, Q₂.

vergleiche: Verfahren zur Minimierung von Automaten (Tabelle zur Markierung nicht äquivalenter Zustände)