Temporale Logik

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

Verfahren

Temporale Logik


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

Beschreibung

Die temporale Logik ist eine spezielle Variante der formalen Logik und dient insbesondere im Bereich des Model Checking zur Spezifikation von Eigenschaften von Systemen, die beispielsweise mit Hilfe von Kripke-Strukturen modelliert wurden. Formeln der temporalen Logik basieren auf atomaren Aussagen und booleschen Operatoren (z. B. ∨, ∧, ¬) zur Beschreibung der Eigenschaften bestimmter Zustände des Modells.

Mit diesen Formeln kann man Folgen von Transitionen zwischen Zuständen in reaktiven Systemen beschreiben, ohne zeitliche Aspekte explizit mit konkreten Zeitangaben zu berücksichtigen. So lassen sich mit Hilfe spezieller temporaler Operatoren und Pfadquantoren beispielsweise Situationen (d.h. Pfade im zum modellierte System gehörigen Berechnungsbaum) beschreiben, in denen bestimmte Zustände "irgendwann" oder "niemals" erreicht werden. Diese temporalen Operatoren und Pfadquantoren können mit booleschen Operatoren kombiniert und beliebig verschachtelt werden.

Es gibt unterschiedliche Varianten der temporalen Logik, die sich in der Verfügbarkeit der temporalen Operatoren und der Pfadquantoren sowie in der Semantik dieser Operatoren unterscheiden. Wichtige Vertreter der temporalen Logik sind

CTL (Computation Tree Logic),
LTL (Linear Temporal Logic) und
CTL* (eine Obermenge von CTL und LTL) sowie
die auf universelle Pfadquantoren eingeschränkten Varianten ACTL und ACTL*.

Diese verschiedenen Varianten der temporalen Logik unterscheiden sich insbesondere durch ihre Ausdrucksmächtigkeit und kommen daher in unterschiedlichen Anwendungsbereichen zum Einsatz.