PLTL: Algorithmen

Satz: die folgenden Fragen sind entscheidbar:

• Modell-Problem:
  • Eingaben: eine PLTL-Formel F über V,
    ein schließlich periodisches Wort w∈Σ^ω mit Σ = $\mathbb {B}$^V
  • Frage: gilt 1 = wert(F, w, 0)
• Erfüllbarkeits-Problem:
  • Eingabe: eine PLTL-Formel F
  • Frage: gibt es w∈Σ^ω mit 1 = wert(F, w, 0)

Beweis-Idee: die Mengen {w∈Σ^ω | 1 = wert(F, w, 0)}

sind ω-regulär (Def. auf nächster Folie)

und lassen sich durch endliche Automaten beschreiben.

(J. R. Büchi 1962, A. Pnueli 1977)