Die Prozeß-Algebra (operationale Semantik)

durch Inferenz-System (= Axiome, Schlußregeln)
für die Übergangsrelation zwischen Prozessen

P₁P₂ bedeutet für a∈Σ: Prozeß P₁ führt a aus (sichtbar) und verhält sich danach wie Prozeß P₂

P₁P₂ bedeutet (mit τ Σ) Prozeß P₁ führt eine nicht sichtbare Aktion aus und verhält sich danach wie Prozeß P₂

• Axiom (a→P)P
• Axiome (P₁ P₂)P₁ und (P₁ P₂)P₂
• Schlußregel:

  wenn PQ, dann (P P')Q und (P' P)Q