Ablehnungs-Semantik

Semantik eines Prozesses ist Menge von Paaren von

• partieller Spur
• und Folge-Menge (mögliche nächste Ereignisse)

dann verschiedene Auswahl-Operatoren:

• external (deterministic) choice $\Box$

  (Umgebung bestimmt, wie es weitergeht)

• internal (nondeterministic) choice $\sqcap$

  (Prozeß entscheidet)