PLTL: propositional linear time logic

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

Johannes Waldmann 2013-02-01