Kripke Strukturen

Sie sind nicht angemeldet

Kompetenzzentrum

Wissensdatenbank

	Anwendungsfelder

	SE-Themen


	Glossar

	Forschungsprojekte

	Anbieterverzeichnis

	Datenbanksuche

	Highlights

Wissensbrowser starten

Einordnung im Wissensnetz

Thema

Formale Methoden

Themeneinstiege

	Activity-Charts
	ATP (Überblick)
	DeadLiveLockVerifISS
	Endlicher Automat
	Entwurf eingeb Systeme
	Formale Logiken
	Model Checking
	Modellbildung
	Petri-Netze (Übersicht)
	Spezifikation
	State-Chart
	Statemate Verifikation
	Symbolic Timing Diagram
	Temporale Logik
	Theorem Proving
	Verifikation

Zuordnung zu SE-Themen

Anforderungen

	Spezifikation

	Validierung

Entwurf

	Notationen

SE Werkzeuge u. Methoden

	Methoden

Verfahren

Kripke Strukturen


	NEU: Externe Quellen zum Thema suchen Externe Quellen werden abgefragt...

Beschreibung

Bei Kripke-Strukturen handelt es sich um einen im Kontext des Model Checking verbreiteten Formalismus zur Beschreibung von Systemmodellen. Kripke-Strukturen bieten die Möglichkeit, einen zustandsbasierten Transitionsgraphen zu definieren, der das Verhalten eines reaktiven Systems festlegt.

Dabei ist eine Kripke-Struktur (KS) wie folgt definiert:

Sei AP eine Menge von atomaren Aussagen. Dann ist eine Kripke-Struktur M über AP ein Tupel M = (S, S₀, R, L) mit:

1. S ist eine endliche Menge von Zuständen. Dabei repräsentiert jeder Zustand eine Belegung innerhalb des zu modellierenden Systems.

2. S₀ ⊆ S ist die Menge der Anfangszustände, d.h. von diesen Zuständen aus darf die Transitionsrelation initial schalten.

3. R ⊆ S x S ist ein totale Transitionsrelation (d.h. für jeden Zustand s ∈ S existiert ein Folgezustand s’ in S mit R(s,s’)), da es somit keinen Endzustand gibt sind die Berechnungspfade von Kripke-Strukturen immer unendlich.

4. L : S → 2^AP ist eine Beschriftungsfunktion, die jeden Zustand auf eine Menge von atomaren Aussagen (Eigenschaften) abbildet. Diese dient dazu die Auswirkungen innerhalb des Systems zu propagieren. Dementsprechend schaltet die KS und die Beschriftungsfunktion nimmt die entsprechenden Systemänderungen in Abhängigkeit der Belegung im aktuellen Zustand vor.

Ein Pfad ist ein endliche Sequenz von Zuständen (durch die Transitionen verbunden) in der Kripke-Struktur: π = s₁s₂... mit s_i ∈ S.

Kripke-Strukturen fallen in die Kategorie der endlichen Automaten, wobei das Ein- und das Ausgabealphabet fehlen und stattdessen die erwähnte Beschriftungsfunktion hinzu kommt.