Nebenläufige Komposition

...mit Synchronisation

• Syntax: (P₁|_SP₂) für S⊆Σ
• Semantik
  • informal: Ereignisse aus S
    sollen in P₁ und P₂ synchron ausgeführt werden,

    Ereignisse S beliebig (asynchron)

  • formal (Inferenzregeln): ...

beachte Spezialfälle S = ∅, S = Σ.