 |
| | | | | Beschreibung | | Bei CTL* handelt es sich um eine temporale Logik, in der es die folgenden beiden grundlegende Arten von Formeln gibt:
- Pfadformeln: Mit diesen Formeln kann man Eigenschaften entlang eines bestimmten Pfades innerhalb des Berechnungsbaumes zu der betrachteten Kripke-Struktur beschreiben.
Die Menge AP enthält alle atomaren Aussagen, die in den Formeln auftreten können. Die Syntax dieser Formeln wird dann mit Hilfe folgender Regeln definiert:
Zustandsformeln:
- Boolesche Operatoren: Wenn f und g Zustandsformeln sind, dann sind auch ¬ f, f ∨ g und f ∧ g Zustandsformeln.
- Pfadquantoren: Wenn f eine Pfadformel ist, dann sind E f und A f Zustandsformeln.
Pfadformeln:
- Zustandsformeln: Wenn f eine Zustandsformel ist, dann ist f auch eine Pfadformel.
- Boolesche und temporale Operatoren: Wenn f und g Pfadformeln sind, dann sind auch ¬ f, f ∨ g, f ∧ g, X f, F f, G f, f U g und f R g Pfadformeln.
Rückkehr zu Temporale Logik | |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | | | | | Syntax von CTL* | | | | | | Weitere Themen | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren