Temporale Logik der Aktionen

Teilgebiet der Informatik

Die Temporale Logik der Aktionen (TLA) (engl. temporal logic of actions) wurde von Leslie Lamport entwickelt. Sie baut zum einen auf der Temporalen Logik (engl. temporal logic) und zum anderen auf der Logik der Aktionen (engl. logic of actions) auf, ist folglich im Ansatz eine Verknüpfung einer Erweiterung der Aussagenlogik durch die Temporale Logik mit der Sprache Logik der Aktionen, in der sich Prädikate, Zustandsfunktionen und Aktionen beschreiben lassen. Es handelt sich um eine Variante der von Amir Pnueli eingeführten temporalen Logik für Programme.

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

Logik der AktionenBearbeiten

Die Logik der Aktionen in der theoretischen Informatik beschäftigt sich mit der Korrektheit von Ausführungen von Computerprogrammen und ermöglicht die Untersuchung der Korrektheit von Programmen.[1]

NotationsgrundlagenBearbeiten

  • Sei   ein syntaktisches Objekt, dann ist   seine semantische Bedeutung.
  •   ist eine andere Schreibweise für   und bedeutet „gleich per definitionem“.
  •   bedeutet, dass   durch   ersetzt wird.

Variablen, Werte und ZuständeBearbeiten

Die Logik der Aktionen verwendet die folgenden drei Klassen:

  – die Klasse aller Variablennamen
  – die Klasse aller möglichen Werte für die Variablen (z. B. 10, „string“,  )
  – die Klasse aller möglichen Zustände

Ein Zustand ist eine Abbildung  , das heißt, der Variablen   wird der Zustand   zugewiesen. Die Zustände beschreiben die Semantik. Man verwendet   statt  . Mit   bezeichnet man somit die Abbildung  .

Somit ist die Schreibweise   in polnischer Notation und bedeutet Anwendung von  .[2]

ZustandsfunktionBearbeiten

Eine Zustandsfunktion (engl. state function) ist ein nicht-boolescher Ausdruck aus Variablen und Konstanten, zum Beispiel  , dazu gehören auch Variablen   (da eine Variable als die Identitätsabbildung   interpretiert werden kann). Der Ausdruck   ist dann die Abbildung  , das heißt,   oder   ist eine Abbildung, die dem Zustand   den Wert   zuordnet. Die Notation   bezeichnet den Wert, den   dem Zustand   zuordnet.

Die semantische Definition von   lautet[3]

 .

Der Ausdruck   bedeutet somit den Wert von  , wenn man alle   durch   ersetzt.

Zusammenfassend:

Zustand    
Zustandsfunktion    
Semantik    

ZustandsprädikatBearbeiten

Ein boolescher Ausdruck   aus Variablen und Konstanten wird Zustandsprädikat (oder kurz Prädikat) genannt, ein Beispiel ist der Ausdruck  . Mit   bezeichnet man die Abbildung   und   ordnet entweder   oder   dem Zustand   zu. Wenn   gilt, dann sagt man   erfüllt das Prädikat  .[3]

Aktion und SchritteBearbeiten

Eine Aktion   ist ein boolescher Ausdruck, der die Beziehung zwischen einem alten Zustand   und einem neuen Zustand   beschreibt. Die Aktion besteht aus „alten Variablen“ und „neuen Variablen“, wobei letztere mit einem   markiert sind. Zum Beispiel ist   eine Aktion, die sagt, dass   im alten Zustand um   größer ist als   im neuen Zustand.

Der Ausdruck   beschreibt die Beziehung zwischen zwei Zuständen, das heißt einen binären Operator, der den beiden Zuständen   einen booleschen Wert   zuweist, dabei wird per definitionem links der alte Zustand und rechts der neue Zustand geschrieben. Die semantische Bedeutung   von   erhält man, indem man   durch   und   durch   ersetzt. Ist  , dann nennt man   einen  -Schritt (engl.  -step).

Der Ausdruck   bedeutet somit das Gleiche wie der boolesche Ausdruck  .

Die semantische Definition von   lautet

 .

Variablen die unterschiedliche Werte in verschiedenen Zuständen besitzen können, werden flexible Variablen (engl. flexible variables) genannt. Variablen die konstant bleiben (aber auch unbekannt sein könne) werden rigide Variablen (engl. rigid variables) genannt. Beispielsweise sei   eine flexible Variable, dann besitzt die Aktion

 

zwei rigide Variablen  , die nicht verändert werden.

Prädikat als AktionBearbeiten

Ein Prädikat kann als Aktion ohne Variablen mit   verstanden werden. Die Aktion   ist gleich dem booleschen Ausdruck   für alle  . Für Zustandsfunktionen und Prädikate   definiert man   als den Ausdruck, den man erhält, wenn man alle Variablen durch deren neue Variable ersetzt, das heißt also

 .

Des Weiteren ist   der gleiche Ausdruck wie  , für alle Zustände  .

Beweisbarkeit und GültigkeitBearbeiten

Eine Aktion   ist gültig (engl. valid), geschrieben   (siehe Tautologie), falls jeder Schritt ein  -Schritt ist, dass heißt also,   ist   für alle  . Die semantische Definition lautet

 

und für ein Prädikat  

 .

Ein Beispiel für eine gültige Aussage ist

 .

Beweisbare Formeln   werden wie in der mathematischen Logik mit   notiert (siehe Ableitung).

Enabled-PrädikateBearbeiten

Sei   eine Aktion, dann ist   ein Prädikat, das genau dann für einen Zustand wahr ist, falls es in dem Zustand möglich ist, einen  -Schritt auszuführen. Die semantische Definition lautet[4]

 

für jeden Zustand  .

Temporale LogikBearbeiten

Die temporale Logik ist ein System von Regeln und Symbolen, durch die man zeitliche Abläufe erfassen kann. Die Semantik der temporalen Logic baut auf „Verhalten“ (engl. behaviors) auf, wobei damit eine unendliche Folge von Zuständen gemeint ist.[5]

Temporale FormelnBearbeiten

Temporale Formeln bestehen aus elementaren Formeln sowie booleschen Operatoren und dem unären Operator  , der „immer“ (engl. always) oder „global“ (engl. global) bedeutet. Mit   wird der boolesche Ausdruck bezeichnet, den das   dem Verhalten   zuweist. Mit   wird das Verhalten bezeichnet, das im Zustand   beginnt. Man sagt   erfüllt   genau dann, wenn  .

Da alle booleschen Ausdrücke durch   und   beschrieben werden können, genügt es, die Ausdrücke   und   zu definieren. Die semantischen Definitionen sind somit[6]

 
 
 

wobei der erste Ausdruck bedeutet, dass ein Verhalten   erfüllt, falls es beide Formeln   und   erfüllt. Der zweite Ausdruck bedeutet, dass das Verhalten   erfüllt, wenn es   nicht erfüllt. Die linke Seite des dritten Ausdruckes   bedeutet, dass die Formel   ab Zustand   gültig ist. Das heißt, die letzte Definition sagt, dass   immer gültig ist (da es per Induktionsschritt definiert ist).[3]

Schlussendlich-OperatorBearbeiten

Die Formel   bedeutet, dass   nicht immer falsch ist und wird mit   abgekürzt und schlussendlich (engl. eventually) genannt:

 

Die Formel   bedeutet, dass   schlussendlich immer wahr ist.

GültigkeitBearbeiten

Eine temporale Formel   ist gültig, falls jedes Verhalten die Formel erfüllt:

 

Temporale Logik der AktionenBearbeiten

Die temporale Logik der Aktionen erhält man, wenn temporale Formeln Aktionen sein können. Die Formeln der TLA bestehen somit aus den logischen Operatoren sowie dem temporalen Operator  .

Ein einfaches BeispielBearbeiten

Gegeben sei ein Algorithmus, der im Zustand   und   beginnt und dann nichtdeterministisch entweder   inkrementiert und   dekrementiert, oder umgekehrt. Als TLA würde das so aussehen:

 
 
 
 
 

Dabei bezeichnet   eine Formel,   den Initialzustand und   eine Aktion.

Stotternde SchritteBearbeiten

Als stotternde Schritte (engl. stuttering steps) werden Schritte bezeichnet, die das Programm pausieren. In dem Beispiel oben würde das bedeuten, dass   und   nicht verändert werden. Ein solcher Schritt lässt sich zum Beispiel so implementieren:[7]

 
 
 
 
 
 

Um stotternde Schritte einfach zu beschreiben, führt man weitere Notationen ein. Mit der Notation   wird   bezeichnet und statt   zu schreiben, notiert man einfach  . Für eine Zustandsfunktion   und eine Aktion   definieren wir:

 

Dann bedeutet   somit:

 

Somit lassen sich die beiden Zeilen

 
 

vereinfachen zu

 .

Syntax und SemantikBearbeiten

Für die TLA gelten die Symbole der booleschen Algebra sowie alle oben definierten Ausdrücke und zusätzlich

     
     

wobei   eine Aktion ist,   eine Zustandsfunktion ist und durch Anwendung logischer Gesetze   gilt.

Für die Formel-Syntax gilt:

 

 

                             

Das Symbol   ist als Trennungszeichen zu verstehen.

VerhaltenseigenschaftenBearbeiten

Eine Sicherheitseigenschaft (engl. safety property) garantiert, dass unerwünschte Zustände nicht passieren. Zum Beispiel ist der durch   spezifizierte Start eine Sicherheitseigenschaft.

Eine Lebendigkeitseigenschaft (engl. liveness property) garantiert, dass erwünschte Zustände erreicht werden, was mit dem   formuliert werden kann. Möchte man eine Fairness und dass zwei Eigenschaften unendlich Mal wiederholt werden, so verwendet man stattdessen  . Somit würde man im obigen Beispiel Folgendes erhalten:

 

Schwache und starke FairnessBearbeiten

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 ihre Ausführung ab einem bestimmten Zeitpunkt immer möglich ist.

Starke Fairness   (engl. strong fairness, compassion) bedeutet, dass eine Aktion ausgeführt werden muss, wenn ihre Ausführung so oft möglich ist.

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

LiteraturBearbeiten

  • Leslie Lamport: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, Band 16, Mai 1994, S. 872–892 (PDF; 485 kB).
  • Leslie Lamport: Introduction to TLA. Digital System Research Center, Palo Alto 1997 (PDF; 121 kB).

WeblinksBearbeiten

Siehe auchBearbeiten

EinzelnachweiseBearbeiten

  1. Krister Segerberg, John-Jules Meyer, Marcus Kracht, Edward N. Zalta: The Logic of Action. In: The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, 2020, abgerufen am 25. September 2021 (englisch).
  2. Leslie Lamport: The Temporal Logic of Actions. In: ACM Transactions on Programming Languages and Systems, Vol. 16. Nr. 3, 1994, S. 875, doi:10.1145/177492.177726 (PDF; 485 kB).
  3. a b c Leslie Lamport: The Temporal Logic of Actions. In: ACM Transactions on Programming Languages and Systems, Vol. 16. Nr. 3, 1994, doi:10.1145/177492.177726 (PDF; 485 kB).
  4. Leslie Lamport: The Temporal Logic of Actions. In: ACM Transactions on Programming Languages and Systems, Vol. 16. Nr. 3, 1994, S. 877, doi:10.1145/177492.177726 (PDF; 485 kB).
  5. Zahar Manna, Amir Pnueli: The Temporal Logic of Reactive and Concurrent Systems. Hrsg.: Springer Verlag. 1992, S. 179, doi:10.1007/978-1-4612-0931-7.
  6. Leslie Lamport: The Temporal Logic of Actions. In: ACM Transactions on Programming Languages and Systems, Vol. 16. Nr. 3, 1994, S. 878, doi:10.1145/177492.177726 (PDF; 485 kB).
  7. Leslie Lamport: The Temporal Logic of Actions. In: ACM Transactions on Programming Languages and Systems, Vol. 16. Nr. 3, 1994, S. 881–882, doi:10.1145/177492.177726 (PDF; 485 kB).