 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Prädikatenlogik erster Ordnung |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Die Prädikatenlogik erster Ordnung (engl. "first order logics") dient im Rahmen des Model Checking der Beschreibung von Zuständen und Transitionen.
Dabei ist für das Verständnis des Model Checking nur eine Teilmenge der Logik erster Ordnung notwendig. Diese umschließt einerseits die logischen Konnektoren (∧, ∨, → etc.) sowie All- (∀) und Existenzquantor (∃). Zustände aus dem Kontext des Model Checking lassen sich mittels logischer Formeln vergleichsweise einfach beschreiben, da ein Zustand eine Belegung von Systemvariablen darstellt und man aus dieser Belegung eine Formel abgeleitet kann. Beispiel: Bei der Belegung ‹v1 ← 2, v2 ← 5, v3 ← 1›. sieht eine (mögliche) korrekte Formel der Logik erster Ordnung folgendermaßen aus: (v1 = 2) ∧ (v2 = 5) ∧ (v3 = 1) oder auch (v1 = 2) ∧ (v2 = 5). Durch die letzte Formel deutet sich bereits an, dass eine Formel auch für mehrere Zustände benutzt werden kann. Allgemein gesagt repräsentiert eine Formel eine Menge von Belegungen, die sie wahr machen. Analog kann die Logik erster Ordnung zur Beschreibung von Transitionen benutzt werden, wobei in diesem Fall zwei Mengen von Belegungen beschrieben werden müssen, nämlich die Zustände vor und nach der Ausführung der Transition. Dementsprechend existieren ungestrichene (unprimed) und gestrichene (primed) Variablen, die die Werte der Systemvariablen vor (unprimed) und nach (primed) Ausführung der Transition enthalten. Beispiel: Die Transition zu der Zuweisungsanweisung x := ( x + y) mod 2 wäre mit Hilfe der Logik erster Ordnung mit folgender Relation korrekt beschrieben: R(x,y,x',y') ≡ x' = (x + y) mod 2 ∧ y' = y | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Prädikatenlogik erster... | ||||
| ||||
| ||||
| ||||
| ||||
| Ansprechpartner | | ||
| ||||
|
| | ||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
| ||||
| Glossar | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
