Übung PLTL

• Ist die Struktur 0(001)^ω ein Modell der Formel $\Diamond$$\Box$p ?
• Gibt es ein Modell für $\Box$(p$\iff$$\Diamond$¬p)?
• Formalisieren Sie (mit den Variablen p_i für „Prozeß i besitzt Ressource``)
  • F = Prozeß 1 besitzt die Ressource unendlich oft,
  • G = Prozesse 1 und 2 besitzen die Ressource nie gleichzeitig,
  • H = immer, wenn Prozeß 1 die Ressource besitzt, dann besitzt Prozeß 2 diese nicht, wird sie aber später erhalten.
• Für alle 8 Konjunktionen von {F, G, H,¬F,¬G,¬H}: geben Sie jeweils ein Modell als ω-reguläres Wort an (falls möglich).
• durch die Operatoren
  • F$\mathsf {U}$ G:

    Es gibt einen Zeitpunkt, zu dem G gilt. Bis dahin gilt F.

  • $\mathsf {X}$ F: im nächsten Zeitpunkt gilt F.
  wird PLTL erweitert.
  • Gegeben Sie die formale Semantik von $\mathsf {U}$ und $\mathsf {X}$ an.
  • Wie kann man $\Diamond$ durch Until realisieren?
  • Realisieren Sie Until durch Next (mit einer Hilfsvariablen p, die weder in F noch in G vorkommt)

    p↔(F$\mathsf {U}$ G) gdw. G∨...