 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Kripke Strukturen (Motivation) |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Kripke Strukturen (KS) sind der (formale) "Standardweg", um im Rahmen des Model Checking auf Basis der Prädikatenlogik erster Ordnung einen Automaten zu konstruieren, der entsprechend den definierten Transitionen schaltet und somit das Verhalten des zu modellierenden Systems (i.d.R. mit parallelen Prozessen) festlegt.
Die Motivation zur Verwendung von KS kommt von der Herangehensweise über die Prädikatenlogik erster Ordnung. Dabei werden Zustände wie auch Transitionen mittels Formeln der Logik erster Ordnung ausgedrückt, welche dann automatisch über geeignete Transformationsregeln in entsprechende KS transformiert werden können. Rückkehr zu Kripke Strukturen | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Kripke Strukturen (Motivation) | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
