www.wikidata.de-de.nina.az

Temporale Logik der Aktionen Die TLA englisch temporal logic of actions wurde von Leslie Lamport entwickelt Sie baut zum

Temporale Logik der Aktionen

Die Temporale Logik der Aktionen (TLA, englisch 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 Aktionen Bearbeiten

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.

Notationsgrundlagen Bearbeiten

  • 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ände Bearbeiten

Die Logik der Aktionen verwendet die folgenden drei Klassen:

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 .

Zustandsfunktion Bearbeiten

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

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

Zusammenfassend:

Zustand
Zustandsfunktion
Semantik

Zustandsprädikat Bearbeiten

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 .

Aktion und Schritte Bearbeiten

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 Aktion Bearbeiten

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ültigkeit Bearbeiten

Eine Aktion ist gültig (engl. valid), geschrieben (siehe Tautologie), falls jeder Schritt ein -Schritt ist, das 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ädikate Bearbeiten

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

für jeden Zustand .

Temporale Logik Bearbeiten

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.

Temporale Formeln Bearbeiten

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

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).

Schlussendlich-Operator Bearbeiten

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ültigkeit Bearbeiten

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

Temporale Logik der Aktionen Bearbeiten

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 Beispiel Bearbeiten

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 Schritte Bearbeiten

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:

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 Semantik Bearbeiten

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.

Verhaltenseigenschaften Bearbeiten

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 Fairness Bearbeiten

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.

Siehe auch Bearbeiten

Literatur Bearbeiten

  • 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).

Weblinks Bearbeiten

Einzelnachweise Bearbeiten

  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 (azurewebsites.net [PDF; 485 kB]).
  3. ↑ 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 (azurewebsites.net [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 (azurewebsites.net [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 (azurewebsites.net [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 (azurewebsites.net [PDF; 485 kB]).
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Die Temporale Logik der Aktionen TLA englisch 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 Verknupfung einer Erweiterung der Aussagenlogik durch die Temporale Logik mit der Sprache Logik der Aktionen in der sich Pradikate Zustandsfunktionen und Aktionen beschreiben lassen Es handelt sich um eine Variante der von Amir Pnueli eingefuhrten temporalen Logik fur 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 mogliche und korrekte Verhalten eines Systems beschreibt Anhand dieser logischen Formel konnen Systeme auf unerwunschte und gewunschte Eigenschaften gepruft werden Inhaltsverzeichnis 1 Logik der Aktionen 1 1 Notationsgrundlagen 1 2 Variablen Werte und Zustande 1 3 Zustandsfunktion 1 4 Zustandspradikat 1 5 Aktion und Schritte 1 5 1 Pradikat als Aktion 1 6 Beweisbarkeit und Gultigkeit 1 7 Enabled Pradikate 2 Temporale Logik 2 1 Temporale Formeln 2 1 1 Schlussendlich Operator 2 2 Gultigkeit 3 Temporale Logik der Aktionen 3 1 Ein einfaches Beispiel 3 2 Stotternde Schritte 3 3 Syntax und Semantik 3 4 Verhaltenseigenschaften 3 4 1 Schwache und starke Fairness 4 Siehe auch 5 Literatur 6 Weblinks 7 EinzelnachweiseLogik der Aktionen BearbeitenDie Logik der Aktionen in der theoretischen Informatik beschaftigt sich mit der Korrektheit von Ausfuhrungen von Computerprogrammen und ermoglicht die Untersuchung der Korrektheit von Programmen 1 Notationsgrundlagen Bearbeiten Sei F displaystyle F nbsp ein syntaktisches Objekt dann ist F displaystyle F nbsp seine semantische Bedeutung displaystyle hat nbsp ist eine andere Schreibweise fur displaystyle nbsp und bedeutet gleich per definitionem s v v displaystyle s v v nbsp bedeutet dass v displaystyle v nbsp durch s v displaystyle s v nbsp ersetzt wird Variablen Werte und Zustande Bearbeiten Die Logik der Aktionen verwendet die folgenden drei Klassen Var displaystyle textbf Var nbsp die Klasse aller Variablennamen Val displaystyle textbf Val nbsp die Klasse aller moglichen Werte fur die Variablen z B 10 string True displaystyle operatorname True nbsp St displaystyle textbf St nbsp die Klasse aller moglichen ZustandeEin Zustand ist eine Abbildung s Var Val x s x displaystyle s colon textbf Var to textbf Val x mapsto s x nbsp das heisst der Variablen x displaystyle x nbsp wird der Zustand s x displaystyle s x nbsp zugewiesen Die Zustande beschreiben die Semantik Man verwendet s x displaystyle s x nbsp statt s x displaystyle s x nbsp Mit x displaystyle x nbsp bezeichnet man somit die Abbildung x St Val displaystyle x colon textbf St to textbf Val nbsp Somit ist die Schreibweise s x displaystyle s x nbsp in polnischer Notation und bedeutet Anwendung von s displaystyle s nbsp 2 Zustandsfunktion Bearbeiten Eine Zustandsfunktion engl state function ist ein nicht boolescher Ausdruck aus Variablen und Konstanten zum Beispiel f x 2 y 4 displaystyle f x 2 y 4 nbsp dazu gehoren auch Variablen x displaystyle x nbsp da eine Variable als die Identitatsabbildung x x displaystyle x mapsto x nbsp interpretiert werden kann Der Ausdruck f displaystyle f nbsp ist dann die Abbildung f St Val s s f displaystyle f colon textbf St to textbf Val s mapsto s f nbsp das heisst f displaystyle f nbsp oder x 2 y 4 displaystyle x 2 y 4 nbsp ist eine Abbildung die dem Zustand s displaystyle s nbsp den Wert s x 2 s y 4 displaystyle left s x right 2 s y 4 nbsp zuordnet Die Notation s f displaystyle s f nbsp bezeichnet den Wert den f displaystyle f nbsp dem Zustand s displaystyle s nbsp zuordnet Die semantische Definition von s f displaystyle s f nbsp lautet 3 s f f v s v v displaystyle s f hat f forall v colon s v v nbsp Der Ausdruck f v s v v displaystyle f forall v colon s v v nbsp bedeutet somit den Wert von f displaystyle f nbsp wenn man alle v displaystyle v nbsp durch s v displaystyle s v nbsp ersetzt Zusammenfassend Zustand s displaystyle s nbsp Var Val x s x s x displaystyle textbf Var to textbf Val x mapsto s x s x nbsp Zustandsfunktion f displaystyle f nbsp x 2 y 4 displaystyle x 2 y 4 nbsp Semantik f displaystyle f nbsp St Val s s f s x 2 s y 4 displaystyle textbf St to textbf Val s mapsto s f s x 2 s y 4 nbsp Zustandspradikat Bearbeiten Ein boolescher Ausdruck P displaystyle P nbsp aus Variablen und Konstanten wird Zustandspradikat oder kurz Pradikat genannt ein Beispiel ist der Ausdruck x 3 y displaystyle x 3 y nbsp Mit P displaystyle P nbsp bezeichnet man die Abbildung P St Booleans displaystyle P colon textbf St to operatorname Booleans nbsp und s P displaystyle s P nbsp ordnet entweder True displaystyle operatorname True nbsp oder False displaystyle operatorname False nbsp dem Zustand s displaystyle s nbsp zu Wenn s P True displaystyle s P operatorname True nbsp gilt dann sagt man s displaystyle s nbsp erfullt das Pradikat P displaystyle P nbsp 3 Aktion und Schritte Bearbeiten Eine Aktion A displaystyle mathcal A nbsp ist ein boolescher Ausdruck der die Beziehung zwischen einem alten Zustand s displaystyle s nbsp und einem neuen Zustand t displaystyle t nbsp beschreibt Die Aktion besteht aus alten Variablen und neuen Variablen wobei letztere mit einem displaystyle nbsp markiert sind Zum Beispiel ist x 2 y displaystyle x 2 y nbsp eine Aktion die sagt dass y displaystyle y nbsp im alten Zustand um 2 displaystyle 2 nbsp grosser ist als x displaystyle x nbsp im neuen Zustand Der Ausdruck A displaystyle mathcal A nbsp beschreibt die Beziehung zwischen zwei Zustanden das heisst einen binaren Operator der den beiden Zustanden s t displaystyle s t nbsp einen booleschen Wert s A t displaystyle s mathcal A t nbsp zuweist dabei wird per definitionem links der alte Zustand und rechts der neue Zustand geschrieben Die semantische Bedeutung s A t displaystyle s mathcal A t nbsp von A displaystyle mathcal A nbsp erhalt man indem man v displaystyle v nbsp durch s v displaystyle s v nbsp und v displaystyle v nbsp durch t v displaystyle t v nbsp ersetzt Ist s A t True displaystyle s mathcal A t operatorname True nbsp dann nennt man s t displaystyle s t nbsp einen A displaystyle mathcal A nbsp Schritt engl A displaystyle mathcal A nbsp step Der Ausdruck s y x 1 t displaystyle s y x 1 t nbsp bedeutet somit das Gleiche wie der boolesche Ausdruck s y t x 1 displaystyle s y t x 1 nbsp Die semantische Definition von s A t displaystyle s mathcal A t nbsp lautet s A t A v s v v t v v displaystyle s mathcal A t hat mathcal A forall v colon s v v t v v nbsp Variablen die unterschiedliche Werte in verschiedenen Zustanden besitzen konnen werden flexible Variablen engl flexible variables genannt Variablen die konstant bleiben aber auch unbekannt sein konne werden rigide Variablen engl rigid variables genannt Beispielsweise sei x displaystyle x nbsp eine flexible Variable dann besitzt die Aktion m N m x n x displaystyle exists m in mathbb N colon mx n x nbsp zwei rigide Variablen m n displaystyle m n nbsp die nicht verandert werden Pradikat als Aktion Bearbeiten Ein Pradikat kann als Aktion ohne Variablen mit displaystyle nbsp verstanden werden Die Aktion s P t displaystyle s P t nbsp ist gleich dem booleschen Ausdruck s P displaystyle s P nbsp fur alle s t displaystyle s t nbsp Fur Zustandsfunktionen und Pradikate F displaystyle F nbsp definiert man F displaystyle F nbsp als den Ausdruck den man erhalt wenn man alle Variablen durch deren neue Variable ersetzt das heisst also F F v v v displaystyle F hat F forall v colon v v nbsp Des Weiteren ist s P t displaystyle s P t nbsp der gleiche Ausdruck wie t P displaystyle t P nbsp fur alle Zustande s t displaystyle s t nbsp Beweisbarkeit und Gultigkeit Bearbeiten Eine Aktion A displaystyle mathcal A nbsp ist gultig engl valid geschrieben A displaystyle vDash mathcal A nbsp siehe Tautologie falls jeder Schritt ein A displaystyle mathcal A nbsp Schritt ist das heisst also s A t displaystyle s mathcal A t nbsp ist True displaystyle operatorname True nbsp fur alle s t St displaystyle s t in textbf St nbsp Die semantische Definition lautet A s t St s A t displaystyle vDash mathcal A hat forall s t in textbf St colon s mathcal A t nbsp und fur ein Pradikat P displaystyle P nbsp P s St s P displaystyle vDash P hat forall s in textbf St colon s P nbsp Ein Beispiel fur eine gultige Aussage ist x y N x y x y displaystyle x y in mathbb N implies x y geq x y nbsp Beweisbare Formeln F displaystyle F nbsp werden wie in der mathematischen Logik mit F displaystyle vdash F nbsp notiert siehe Ableitung Enabled Pradikate Bearbeiten Sei A displaystyle mathcal A nbsp eine Aktion dann ist E n a b l e d A displaystyle Enabled mathcal A nbsp ein Pradikat das genau dann fur einen Zustand wahr ist falls es in dem Zustand moglich ist einen A displaystyle mathcal A nbsp Schritt auszufuhren Die semantische Definition lautet 4 s E n a b l e d A t St s A t displaystyle s Enabled mathcal A hat exists t in textbf St colon s mathcal A t nbsp fur jeden Zustand s displaystyle s nbsp Temporale Logik BearbeitenDie temporale Logik ist ein System von Regeln und Symbolen durch die man zeitliche Ablaufe erfassen kann Die Semantik der temporalen Logic baut auf Verhalten engl behaviors auf wobei damit eine unendliche Folge von Zustanden gemeint ist 5 Temporale Formeln Bearbeiten Temporale Formeln bestehen aus elementaren Formeln sowie booleschen Operatoren und dem unaren Operator displaystyle square nbsp der immer engl always oder global engl global bedeutet Mit s F displaystyle sigma F nbsp wird der boolesche Ausdruck bezeichnet den das F displaystyle F nbsp dem Verhalten s displaystyle sigma nbsp zuweist Mit s 0 s 1 displaystyle langle s 0 s 1 dots rangle nbsp wird das Verhalten bezeichnet das im Zustand s 0 displaystyle s 0 nbsp beginnt Man sagt s displaystyle sigma nbsp erfullt F displaystyle F nbsp genau dann wenn s F True displaystyle sigma F operatorname True nbsp Da alle booleschen Ausdrucke durch displaystyle wedge nbsp und displaystyle lnot nbsp beschrieben werden konnen genugt es die Ausdrucke F F G displaystyle lnot F F wedge G nbsp und F displaystyle square F nbsp zu definieren Die semantischen Definitionen sind somit 6 s F G s F s G displaystyle sigma F land G hat sigma F land sigma G nbsp s F s F displaystyle sigma lnot F hat lnot sigma F nbsp s 0 s 1 F n N s n s n 1 s n 2 F displaystyle langle s 0 s 1 dots rangle square F hat forall n in mathbb N langle s n s n 1 s n 2 dots rangle F nbsp wobei der erste Ausdruck bedeutet dass ein Verhalten F G displaystyle F land G nbsp erfullt falls es beide Formeln F displaystyle F nbsp und G displaystyle G nbsp erfullt Der zweite Ausdruck bedeutet dass das Verhalten F displaystyle lnot F nbsp erfullt wenn es F displaystyle F nbsp nicht erfullt Die linke Seite des dritten Ausdruckes s 0 s 1 F displaystyle langle s 0 s 1 dots rangle square F nbsp bedeutet dass die Formel F displaystyle F nbsp ab Zustand s 0 displaystyle s 0 nbsp gultig ist Das heisst die letzte Definition sagt dass F displaystyle F nbsp immer gultig ist da es per Induktionsschritt definiert ist 3 Schlussendlich Operator Bearbeiten Die Formel F displaystyle lnot square lnot F nbsp bedeutet dass F displaystyle F nbsp nicht immer falsch ist und wird mit F displaystyle Diamond F nbsp abgekurzt und schlussendlich engl eventually genannt F F displaystyle Diamond F hat lnot square lnot F nbsp Die Formel F displaystyle Diamond square F nbsp bedeutet dass F displaystyle F nbsp schlussendlich immer wahr ist Gultigkeit Bearbeiten Eine temporale Formel F displaystyle F nbsp ist gultig falls jedes Verhalten die Formel erfullt F s St s F displaystyle vDash F hat forall sigma in textbf St infty colon sigma F nbsp Temporale Logik der Aktionen BearbeitenDie temporale Logik der Aktionen erhalt man wenn temporale Formeln Aktionen sein konnen Die Formeln der TLA bestehen somit aus den logischen Operatoren sowie dem temporalen Operator displaystyle square nbsp Ein einfaches Beispiel Bearbeiten Gegeben sei ein Algorithmus der im Zustand x 0 displaystyle x 0 nbsp und z 0 displaystyle z 0 nbsp beginnt und dann nichtdeterministisch entweder x displaystyle x nbsp inkrementiert und z displaystyle z nbsp dekrementiert oder umgekehrt Als TLA wurde das so aussehen I n i t ϕ x 0 z 0 displaystyle Init phi hat x 0 wedge z 0 nbsp A 1 x x 1 z z 1 displaystyle mathcal A 1 hat x x 1 wedge z z 1 nbsp A 2 x x 1 z z 1 displaystyle mathcal A 2 hat x x 1 wedge z z 1 nbsp A A 1 A 2 displaystyle mathcal A hat mathcal A 1 vee mathcal A 2 nbsp ϕ I n i t ϕ A displaystyle phi hat Init phi wedge square mathcal A nbsp Dabei bezeichnet ϕ displaystyle phi nbsp eine Formel I n i t ϕ displaystyle Init phi nbsp den Initialzustand und A displaystyle mathcal A nbsp eine Aktion Stotternde Schritte Bearbeiten Als stotternde Schritte engl stuttering steps werden Schritte bezeichnet die das Programm pausieren In dem Beispiel oben wurde das bedeuten dass x displaystyle x nbsp und z displaystyle z nbsp nicht verandert werden Ein solcher Schritt lasst sich zum Beispiel so implementieren 7 I n i t ϕ x 0 z 0 displaystyle Init phi hat x 0 wedge z 0 nbsp A 1 x x 1 z z 1 displaystyle mathcal A 1 hat x x 1 wedge z z 1 nbsp A 2 x x 1 z z 1 displaystyle mathcal A 2 hat x x 1 wedge z z 1 nbsp S 1 x x z z displaystyle mathcal S 1 hat x x wedge z z nbsp A A 1 A 2 displaystyle mathcal A hat mathcal A 1 vee mathcal A 2 nbsp ϕ I n i t ϕ A S 1 displaystyle phi hat Init phi wedge square mathcal A vee mathcal S 1 nbsp Um stotternde Schritte einfach zu beschreiben fuhrt man weitere Notationen ein Mit der Notation x z x z displaystyle langle x z rangle langle x z rangle nbsp wird x x z z displaystyle x x wedge z z nbsp bezeichnet und statt x z displaystyle langle x z rangle nbsp zu schreiben notiert man einfach x z displaystyle langle x z rangle nbsp Fur eine Zustandsfunktion f displaystyle f nbsp und eine Aktion A displaystyle mathcal A nbsp definieren wir A f A f f displaystyle mathcal A f hat mathcal A vee f f nbsp Dann bedeutet M x z displaystyle mathcal M langle x z rangle nbsp somit M x z M x z x z M x x z z M S 1 displaystyle mathcal M langle x z rangle mathcal M vee langle x z rangle langle x z rangle mathcal M vee x x wedge z z mathcal M vee mathcal S 1 nbsp Somit lassen sich die beiden Zeilen S 1 x x z z displaystyle mathcal S 1 hat x x wedge z z nbsp ϕ I n i t ϕ A S 1 displaystyle phi hat Init phi wedge square mathcal A vee mathcal S 1 nbsp vereinfachen zu ϕ I n i t ϕ A x z displaystyle phi hat Init phi wedge square mathcal A langle x z rangle nbsp Syntax und Semantik Bearbeiten Fur die TLA gelten die Symbole der booleschen Algebra sowie alle oben definierten Ausdrucke und zusatzlich A f displaystyle mathcal A f nbsp displaystyle hat nbsp A f f displaystyle mathcal A lor f f nbsp A f displaystyle langle mathcal A rangle f nbsp displaystyle hat nbsp A f f displaystyle mathcal A land f neq f nbsp wobei A displaystyle mathcal A nbsp eine Aktion ist f displaystyle f nbsp eine Zustandsfunktion ist und durch Anwendung logischer Gesetze A f f A f f displaystyle mathcal A wedge f neq f lnot lnot mathcal A vee f f nbsp gilt Fur die Formel Syntax gilt F o r m e l displaystyle langle Formel rangle nbsp displaystyle hat nbsp F o r m e l F o r m e l displaystyle langle Formel rangle land langle Formel rangle nbsp displaystyle vert nbsp F o r m e l F o r m e l displaystyle langle Formel rangle lor langle Formel rangle nbsp displaystyle vert nbsp F o r m e l displaystyle neg langle Formel rangle nbsp displaystyle vert nbsp F o r m e l displaystyle Box langle Formel rangle nbsp displaystyle vert nbsp F o r m e l displaystyle Diamond langle Formel rangle nbsp displaystyle vert nbsp P r a d i k a t displaystyle langle Pr ddot a dikat rangle nbsp displaystyle vert nbsp A k t i o n f displaystyle Box lbrack Aktion rbrack langle f rangle nbsp displaystyle vert nbsp A k t i o n f displaystyle Box langle Aktion rangle langle f rangle nbsp Das Symbol displaystyle nbsp ist als Trennungszeichen zu verstehen Verhaltenseigenschaften Bearbeiten Eine Sicherheitseigenschaft engl safety property garantiert dass unerwunschte Zustande nicht passieren Zum Beispiel ist der durch I n i t ϕ displaystyle Init phi nbsp spezifizierte Start eine Sicherheitseigenschaft Eine Lebendigkeitseigenschaft engl liveness property garantiert dass erwunschte Zustande erreicht werden was mit dem A displaystyle Diamond square mathcal A nbsp formuliert werden kann Mochte man eine Fairness und dass zwei Eigenschaften unendlich Mal wiederholt werden so verwendet man stattdessen A 1 A 2 displaystyle Diamond square mathcal A 1 wedge Diamond square mathcal A 2 nbsp Somit wurde man im obigen Beispiel Folgendes erhalten ϕ I n i t ϕ A x z A 1 A 2 displaystyle phi hat Init phi wedge square mathcal A langle x z rangle wedge Diamond square mathcal A 1 wedge Diamond square mathcal A 2 nbsp Schwache und starke Fairness Bearbeiten In einem nebenlaufigen System unterscheidet man zwischen schwacher und starker Fairness Schwache Fairness WF displaystyle operatorname WF nbsp engl weak fairness justice bedeutet dass eine Aktion unendlich oft ausgefuhrt werden muss wenn ihre Ausfuhrung ab einem bestimmten Zeitpunkt immer moglich ist Starke Fairness SF displaystyle operatorname SF nbsp engl strong fairness compassion bedeutet dass eine Aktion ausgefuhrt werden muss wenn ihre Ausfuhrung so oft moglich ist Ist ein Verhalten stark fair bezuglich einer Aktion so ist es auch schwach fair fur diese Aktion Siehe auch BearbeitenFormale Systeme Formale Semantik Formale SpracheLiteratur BearbeitenLeslie 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 Weblinks BearbeitenStephan Merz Temporal logic guide englisch TLA The way to specify Community website on TLA and PlusCal englisch Leslie Lamport The TLA Home Page englisch Patricia Ulmer Temporal Logic of Action Memento vom 15 April 2016 im Internet Archive PDF 413 kB Proseminar Ausarbeitung TU Munchen Leslie Lamport My Papers About TLA and TLA Einzelnachweise Bearbeiten 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 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 azurewebsites net PDF 485 kB 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 azurewebsites net PDF 485 kB 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 azurewebsites net PDF 485 kB 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 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 azurewebsites net PDF 485 kB 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 azurewebsites net PDF 485 kB Abgerufen von https de wikipedia org w index php title Temporale Logik der Aktionen amp oldid 231455445