Plan

betrachten Zustandsübergangssysteme allgemein (Beispiele: endliche Automaten, Petri-Netze, CSP)

Semantiken und durch sie definierte Äquivalenzen:

• Spur-Semantik trace(S)⊆Σ^*

  S₁ spur-äquivalent zu S₂, falls trace(S₁) = trace(S₂).

• Ablehnungs-Semantik rej(S)⊆Σ^*×Pow(Σ)

  S₁ ablehnungs-äquivalent zu S₂, falls rej(S₁) = rej(S₂).

• Bisimulation: S₁ bisimilar zu S₂, falls eine Relation (Bisimulation) R⊆(S₁)×(S₂) mit bestimmten Eigenschaften existiert