 |
| | | | | Erläuterung | | Mit Hilfe von temporalen Operatoren kann man im Kontext der temporalen Logik ausgewählte Pfade im Berechnungsbaum einer Kripke-Struktur beschreiben.
Es gibt die folgenden fünf grundlegenden Operatoren:
- X ("next time"): Dieser Operator beschreibt, dass die angegebene Eigenschaft im zweiten Zustand des betrachteten Pfades erfüllt ist.
- F ("eventually" oder "in the future"): Dieser Operator beschreibt, dass die angegebene Eigenschaft in irgendeinem Zustand des betrachteten Pfades erfüllt ist.
- G ("always" oder "globally"): Dieser Operator beschreibt, dass die angegebene Eigenschaft in jedem Zustand des betrachteten Pfades erfüllt ist.
- U ("until"): Dieser Operator kombiniert zwei Eigenschaften zu folgender Aussage: Falls auf dem betrachteten Pfad ein Zustand existiert, in dem die zweite Eigenschaft erfüllt ist, muss in jedem vorherigen Zustand die erste Eigenschaft erfüllt sein.
- R ("release"): Auch dieser Operator kombiniert zwei Eigenschaften und beschreibt folgende zum U-Operator komplementäre Aussage: Die zweite Eigenschaft muss in allen Zuständen entlang des betrachteten Pfades erfüllt sein bis inklusive zu dem ersten Zustand, in dem die erste Eigenschaft erfüllt ist. Es ist jedoch möglich, dass der betrachtete Pfad keinen Zustand enthält, in dem die erste Eigenschaft erfüllt ist. In diesem Fall muss die zweite Eigenschaft in jedem Zustand des Pfades erfüllt sein.
| |
| | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | | | | | Temporale Operatoren | | | | |  | Erläutert Technologien | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
