Temporale Logik der Aktionen

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
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 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.

Symbole[Bearbeiten | Quelltext bearbeiten]

Es gelten die Symbole der booleschen Algebra und weitere Symbole

gleich per Definition
F ist gültig
immer
endlich, schließlich
Aktion (Stotterschritt)
Aktion

Syntax und Semantik[Bearbeiten | Quelltext bearbeiten]

            

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.

ohne gestrichenen Variablen     Enabled(Aktion)

nichtboolescher Ausdruck aus Konstanten, Variablen zur Beschreibung eines Zustandes

Verhalten

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.

ist ein Stotterschritt, der den Wert der Variablen unverändert lässt (engl. stuttering step).

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 ein A step ist. In einem Verhalten ist ein Prädikat nur dann true, wenn es in dem ersten Zustand true ist.

Verhaltenseigenschaften[Bearbeiten | Quelltext bearbeiten]

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[Bearbeiten | Quelltext bearbeiten]

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 zu y 1 addieren.

Damit eine TLA - Spezifikation angegeben werden kann, müssen erst die Zustandsfunktionen und Aktionen definiert werden.

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

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



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


Aus diesen drei Bestandteilen erhalten wir folgende TLA-Formel:




Siehe auch[Bearbeiten | Quelltext bearbeiten]

Weblinks[Bearbeiten | Quelltext bearbeiten]