Temporale Logik der Aktionen

Temporale Logik der Aktionen

Die Temporale Logik der Aktionen (TLA) ist eine Weiterentwicklung der Temporalen Logik (engl. temporal logic) und der Logik der Aktionen (engl. logic of actions). Sie wurde von Leslie Lamport entwickelt.

Die Temporale Logik der Aktionen gehört zur Aussagenlogik (engl. propositional logic) und wird in der Informatik zur Spezifikation, Argumentation und Verifikation von Systemen (z. B. Programmen) verwendet. Eine Spezifikation in TLA ist eine logische Formel, die alle möglichen und korrekten Verhalten eines Systems beschreibt. Anhand dieser logischen Formel können Systeme auf unerwünschte und gewünschte Eigenschaften geprüft werden.

Inhaltsverzeichnis

Symbole

Es gelten die Symbole der booleschen Algebra und weitere Symbole

\hat = gleich per Definition
\models F F ist gültig
\Box immer
\Diamond endlich, schließlich
\circ zum nächsten Zeitpunkt
[A] Aktion ( Stotterschritt )
\langle A \rangle Aktion

Syntax und Semantik

\langle Formel \rangle

 \hat =


\langle Formel \rangle \land \langle Formel \rangle   
 \vert 
\langle Formel \rangle \lor \langle Formel \rangle  
 \vert 
\neg \langle Formel \rangle 
 \vert 
\Box \langle Formel \rangle
 \vert 
\Diamond \langle Formel \rangle
 \vert 
\langle Pr\ddot adikat \rangle
 \vert 
\Box {\lbrack \langle Aktion \rangle \rbrack}_{\langle Zustandsfunktion \rangle}

\langle Aktion \rangle

 \hat =

boolescher Ausdruck aus Konstanten, Variablen und gestrichenen (engl. primed) Variablen. Eine Aktion stellt dabei eine Relation zwischen zwei Zuständen dar, wobei gestrichene Variablen sich auf den neuen Zustand beziehen. Ein Paar von Zuständen die eine Aktion A erfüllen wird A step genannt.

\langle Pr\ddot adikat \rangle

 \hat =

\langle Aktion \rangle ohne gestrichenen Variablen   \vert  Enabled(Aktion)

\langle Zustandsfunktion \rangle

 \hat =

nichtboolescher Ausdruck aus Konstanten, Variablen zur Beschreibung eines Zustandes

Verhalten

 \hat =

unendliche Sequenz von Zuständen


Im folgenden sind z,u Zustände, f Zustandsfunktionen, A Aktionen, F,G Formeln, p Prädikate, v Variablen und σ Verhalten.

Sei f eine Zustandsfunktion oder ein Prädikat, f' ist dann der Ausdruck f, in dem alle Variablen durch gestrichene Variablen ersetzt wurden.

z[f] \hat = f( \forall 'v' : z\lbrack v \rbrack /v )
s[f]u \hat = f( \forall 'v' : z\lbrack v \rbrack / v, u\lbrack v \rbrack /v' )
\models A \hat = \forall z,u : z \lbrack A \rbrack t
\sigma \lbrack F \land G \rbrack \hat = \sigma \lbrack F \rbrack \land \sigma \lbrack G \rbrack
 \sigma \lbrack \neg F \rbrack \hat =  \neg \sigma \lbrack F \rbrack
\models F \hat = \forall \sigma : \sigma \lbrack F \rbrack
[A]f \hat = A \lor ( f' = f )
{\langle A \rangle}_f \hat = A \land ( f' \neq f )

[A]f ist ein Stotterschritt der den Wert der Variablen unverändert lässt (engl. stuttering step).

{\langle A \rangle}_f ist ein Schritt der die Zustandsfunktion verändert.

Für jede Aktion A ist ein Prädikat Enabled A definiert. Es ist in einen Zustand nur dann true , wenn es möglich ist von diesem Zustand aus einen A step auszuführen. d.h. Enabled A ist im Zustand z true , falls ein Zustand u existiert, so dass \langle z,u \rangle ein A step ist. In einem Verhalten ist ein Prädikat nur dann true wenn es in dem ersten Zustand true ist.

Verhaltenseigenschaften

Eine Sicherheitseigenschaft garantiert, dass unerwünschte Zustände niemals erreicht werden.

Eine Lebendigkeitseigenschaft garantiert, dass erwünschte Zustände irgendwann erreicht werden.

In einem nebenläufigen System unterscheidet man zwischen schwacher und starker Fairness. Schwache Fairness (engl. weak fairness, justice) bedeutet, dass eine Aktion unendlich oft ausgeführt werden muss, wenn die Ausführung dieser ab einem bestimmten Zeitpunkt immer möglich ist. Anders: Wird eine Aktion nur endlich oft ausgeführt, so ist diese in einem Verhalten unendlich oft nicht ausführbar. Sie sichert zu, dass die Aktion schließlich ausgeführt wird oder, dass dessen Ausführung unmöglich wird – wenn auch nur für eine bestimmte Zeitspanne.

Starke Fairness (engl. strong fairness, compassion) bedeutet, dass eine Aktion unendlich oft ausgeführt werden muss, wenn die Ausführung dieser unendlich oft möglich ist. Anders: Wird eine Aktion nur endlich oft ausgeführt, so ist diese in einem Verhalten nur endlich oft ausführbar. Es versichert, dass die Aktion schließlich ausgeführt wird oder, dass dessen Ausführung schließlich für immer unmöglich wird.

Ist ein Verhalten stark fair bezüglich einer Aktion, so ist es auch schwach fair für diese Aktion.

Darstellung und Beispiel

var x=0, y=0

doParallel({x:=x+1},{y:=y+1})

Oben stehendes Program in Pseudocode soll in paralleler Verarbeitung (nichtdeterministisch) entweder zu x oder y 1 addieren.

Um eine TLA - Spezifikation angeben zu können, müssen erst die Zustandsfunktionen und Aktionen definiert werden.

In diesem Beispiel reicht ein Zustand, der gleichzeitig der Anfangszustand ist.

Init_\phi = (x=0) \land (y=0)

Die parallel ablaufenden Additionen können in zwei Aktionen M1,M2 beschrieben werden.

M_1 \hat = (x'=x+1) \land (y'=y),

M_2 \hat = (y'=y+1) \land (x'=x),

M = M_1 \lor M_2

Zum Schluss werden noch Fairnessbedingungen spezifiziert. SF als starke Fairness und WF als schwache Fairness.

SF_{\langle x,y \rangle} (M_1)

SF_{\langle x,y \rangle} (M_2)

Aus diesen drei Bestandteilen erhalten wir folgende TLA-Formel:


Init_\phi = (x=0) \land (y=0)

M_1 \hat = (x'=x+1) \land (y'=y) M_2 \hat = (y'=y+1) \land (x'=x)

M = M_1 \lor M_2

\phi \hat = Init_\phi \land \Box {\lbrack M \rbrack}_{\langle x,y \rangle} \land SF_{\langle x,y \rangle} (M_1) \land SF_{\langle x,y \rangle} (M_2)

Siehe auch

Weblinks


Wikimedia Foundation.

Игры ⚽ Нужна курсовая?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Temporale Logik von Aktionen — Dieser Artikel oder Abschnitt bedarf einer Überarbeitung. Näheres ist auf der Diskussionsseite angegeben. Hilf mit, ihn zu verbessern, und entferne anschließend diese Markierung. Die Temporale Logik der Aktionen (TLA) ist eine Weiterentwicklung… …   Deutsch Wikipedia

  • Logik — (von altgriechisch λογική τέχνη logiké téchnē „denkende Kunst“, „Vorgehensweise“) ist die Lehre des vernünftigen (Schluss)Folgerns. Die Logik untersucht die Gültigkeit von Argumenten hinsichtlich ihrer Struktur unabhängig vom konkreten Inhalt der …   Deutsch Wikipedia

  • Aristotelische Logik — Gregor Reisch, „Die Logik präsentiert ihre zentralen Themen“, Margarita Philosophica, 1503/08 (?). Die beiden Hunde veritas und falsitas jagen de …   Deutsch Wikipedia

  • Temporal Logic of Actions — Dieser Artikel oder Abschnitt bedarf einer Überarbeitung. Näheres ist auf der Diskussionsseite angegeben. Hilf mit, ihn zu verbessern, und entferne anschließend diese Markierung. Die Temporale Logik der Aktionen (TLA) ist eine Weiterentwicklung… …   Deutsch Wikipedia

  • Lamport Hash — Leslie Lamport Leslie Lamport (* 7. Februar 1941 in New York) ist ein US amerikanischer Mathematiker, Informatiker und Programmierer. Lamport schloss 1960 am Massachusetts Institute of Technology mit dem Bachelor in Mathematik ab. 1963 erlangte… …   Deutsch Wikipedia

  • Agenten-Programmiersprache — Dieser Artikel oder Abschnitt bedarf einer Überarbeitung. Näheres ist auf der Diskussionsseite angegeben. Hilf mit, ihn zu verbessern, und entferne anschließend diese Markierung. Agentenorientierte Programmierung ist eine Art der Programmierung,… …   Deutsch Wikipedia

  • Leslie Lamport — (* 7. Februar 1941 in New York) ist ein US amerikanischer Mathematiker, Informatiker und Programmierer. Lamport schloss 1960 am Massachusetts Institute of Technology mit dem Bachelor in Mathematik ab. 1963 erlangte er an de …   Deutsch Wikipedia

  • Fairness — geht als Begriff auf das englische Wort „fair“ („anständig“, „ordentlich“) zurück. Fairness drückt eine (nicht gesetzlich geregelte) Vorstellung individueller Gerechtigkeit aus. Fairness lässt sich im Deutschen mit akzeptierter Gerechtigkeit und… …   Deutsch Wikipedia

  • Agentenorientierte Programmierung — ist eine Art der Programmierung, die auf der Theorie der agentenorientierten Paradigmen von Yoav Shoham basiert, und hauptsächlich in der deklarativen Programmiersprache PROLOG angewendet wurde. 1993 hat Shoham agentenorientierte Paradigmen… …   Deutsch Wikipedia

  • State-Chart — Ein Zustandsübergangsdiagramm ist eine grafische Darstellung von endlichen Automaten, d. h. Zuständen und deren Übergangsbedingungen, um die enthaltenen Verknüpfungen möglichst durchschaubar und eindeutig zu visualisieren. Anwendung findet das… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”