PLTL-Spezifikationen von Systemeigenschaften

• gegenseitiger Ausschluß (mutual exclusion):

  Variablen: p_i : = Prozeß i besitzt eine Ressource

  • Spezifikation (2 Prozesse): $\Box$¬(p₁∧p₂)

    
    

  • Übung: für 3 Prozesse lautet die Formel nicht

    $\Box$¬(p₁∧p₂∧p₃). Warum nicht? Wie dann?

• 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)