Bestimmung einer Bisimulation (Impl.)

aus Definition „R ist Bisimulation``:

• S₁-Transitionen durch S₂-Transitionen simuliert:

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

• und symmetrisch ( 1↔2)

leite Verfeinerungsverfahren ab:

gegeben R_k, definiere R_k+1 durch:

(p₁, p₂)∈R_k+1, falls (p₁, p₂)∈R_k und

• ∀(p₁, a, q₁)∈T₁ : ∃q₂ : (p₂, a, q₂)∈T₂∧(q₁, q₂)∈R_k
• und symmetrische Bedingung (tausche 1↔2)