Die Semantik von CTL*-Formeln wird mit bezug auf die zugrundeliegende Kripke Strukturen definiert. Ein Pfad π in einer Kripke-Struktur M = <S, R, L> ist eine unendliche Folge von Zuständen π = s0, s1, ... mit (si, si+1) ∈ R für i ≥ 0.
Mit πi wird der Teilpfad von π bezeichnet, der im Zustand si beginnt. Der Ausdruck M, s |= f bedeutet, dass die Zustandsformel g im Zustand s der Kripke-Struktur M gilt. Entsprechend bedeutet der Ausdruck M, π |= f, dass die Pfadformel g entlang des Pfades π in der Kripke-Struktur M gilt.
Die Relation |= wird für Zustandsformeln g1 und g2 sowie Pfadformeln g1 und g2 folgendermaßen definiert:
- M, s |= p ⇔ p ∈L(s)
- M, s |= ¬g1 ⇔ M, s |≠ g1
- M, s |= g1 ∨ g2 ⇔ M, s |= g1 oder M, s |= g2
- M, s |= g1 ∧ g2 ⇔ M, s |= g1 und M, s |= g2
- M, s |= E g1 ⇔ Es existiert ein im Zustand s beginnender Pfad π mit M, π |= g1
- M, s |= A g1 ⇔ Für jeden im Zustand s beginnenden Pfad π gilt M, π |= g1
- M, π |= g1 ⇔ s ist der erste Zustand von π und M, s |= g1
- M, π |= ¬g1 ⇔ M, π |≠ g1
- M, π |= g1 ∨ g2 ⇔ M, π |= g1 oder M, π |= g2
- M, π |= g1 ∧ g2 ⇔ M, π |= g1 und M, π |= g2
- M, π |= X g1 ⇔ M, π1 |= g1
- M, π |= F g1 ⇔ Es existiert ein k≥0 mit M, πk |= g1
- M, π |= G g1 ⇔ für alle i≥0 gilt M, πi |= g1
- M, π |= g1 U g2 ⇔ Es existiert ein k≥0 mit M, πk |= g2 und für alle 0≤j<k gilt M, πj |= g1
- M, π |= g1 R g2 ⇔ Für alle j≥0 gilt: Falls M, πi |≠ g1 für jedes i<j gilt, dann folgt daraus M, πj |= g2
Offenbar genügen schon die Operatoren ∨, ¬, X, U und E, um jede mögliche CTL*-Formel beschreiben zu können.
Rückkehr zu Temporale Logik |
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren