PLTL: propositional linear time logic

Syntax:

• Variablen p, q,..., logische Operatoren ¬,∨,∧,⇒,...
• temporale Operatoren: immer $\Box$, irgendwann $\Diamond$,...

Beispiele: $\Diamond$(p∨q), $\Box$$\Diamond$p, $\Diamond$$\Box$p

Semantik: Wert der Formel F in Struktur K zur Zeit s:

• für v∈V: wert(v, K, s) = b_K(s)(v)
• wert(F₁∧F₂, K, s) = min{wert(F₁, K, s), wert(F₂, K, s)}
• wert($\Box$F₁, K, s) = min{wert(F₁, K, s') | s'∈$\mathbb {N}$, s'≥s}
• wert($\Diamond$F₁, K, s) = max{wert(F₁, K, s') | s'∈$\mathbb {N}$, s'≥s}

Übung: $\Diamond$$\Box$φ⇒$\Box$$\Diamond$φ ist allgemeingülitg (gilt in jeder Struktur), ...aber die Umkehrung nicht