Kripke-Strukturen, Omega-Wörter

allgemein: Kripke-Struktur zu Variablenmenge V ist

• Graph (S, T) mit S = Menge der Systemzustände, T⊆S×S Menge der Zustandsübergänge
• Knotenbeschriftung b : S→(V→$\mathbb {B}$)

  d.h., b(s) ist eine Belegung der Variablen V

hier speziell:

• S = $\mathbb {N}$ (Zeitpunkte 0, 1,…)
• T = {(s, s + 1) | s∈$\mathbb {N}$} (linear time)

Beispiel:

• V = {p, q},
• b(s) = {(p,(s≥3)),(q,(2 | s))}