 |
| | | | | Erläuterung | | Im Kontext der temporalen Logik wird ein Berechnungsbaum (engl. "computation tree") auf Basis einer Kripke-Struktur folgendermaßen konstruiert:
- Ein Zustand der Kripke-Struktur wird als Startzustand ausgewählt.
- Anschließend wird die (endliche) Kripke-Struktur in einen unendlichen Baum abgerollt, an dessen Wurzel der ausgewählte Startzustand steht.
An einem solchen Berechnungsbaum kann man alle möglichen Ausführungsvarianten des durch die Kripke-Struktur modellierten Systems ablesen, die von dem ausgewählten Startzustand ausgehen. Jede dieser Ausführungsvarianten wird durch einen unendlichen Pfad im Berechnungsbaum repräsentiert, der in der Baumwurzel beginnt.
Ein einfaches Beispiel für die Umwandlung einer Kripke-Struktur in einen zugehörigen Berechnungsbaum ist im folgenden dargestellt.
Die folgende (endliche) Kripke-Struktur mit den drei Zuständen ab, bc und c
wird bei Auswahl des Zustands ab als Startzustand zu folgendem (unendlichen) Berechnungsbaum:
| |
| | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | | | | | Berechnungsbaum | | | | |  | Erläutert Technologien | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
