PLTL-Spezifikationen von Systemeigenschaften

• gegenseitiger Ausschluß (mutual exclusion):

  Variablen: p_i : = Prozeß i besitzt eine Ressource

  Spezifikation: $\Box$¬(p₁∧…∧p_n)

• Fairness (kein Verhungern, no starvation)

  Variablen: A_i : = Prozeß i beantragt Ressource; P_i

  Spezifikation: $\Box$(A₁⇒$\Diamond$P₁)∧…∧$\Box$(A_n⇒$\Diamond$P_n)