Temporal Logic of Actions

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 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 Verfikation 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 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üglicher 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:

  • Temporal logic of actions — (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions.It is used to describe behaviours of concurrent systems.Statements in temporal logic of the form [A] t, where A is an action and t contains a… …   Wikipedia

  • Temporal logic — In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a particular modal logic… …   Wikipedia

  • Interval temporal logic — (also interval logic) is a temporal logic for representing both propositional and first order logical reasoning about periods of time that is capable of handling both sequential and parallel composition. Instead of dealing with infinite sequences …   Wikipedia

  • logic —    Logic is the study of the correct way of reasoning. It is a prescriptive discipline rather than a merely descriptive one (psychology describes how we actually do reason). The two main methods for describing how we should think are the… …   Christian Philosophy

  • Dynamic logic (modal logic) — For the subject in digital electronics also known as clocked logic, see dynamic logic (digital electronics). Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general… …   Wikipedia

  • Lógica temporal — La lógica temporal es una extensión de la lógica modal, la cual es practicamente usada en sistema de reglas, donde esta presente el tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene… …   Wikipedia Español

  • logic — logicless, adj. /loj ik/, n. 1. the science that investigates the principles governing correct or reliable inference. 2. a particular method of reasoning or argumentation: We were unable to follow his logic. 3. the system or principles of… …   Universalium

  • applied logic — Introduction       the study of the practical art of right reasoning. The formalism (formal logic) and theoretical results of pure logic can be clothed with meanings derived from a variety of sources within philosophy as well as from other… …   Universalium

  • Mill, John Stuart: Logic and metaphysics — J.S.Mill Logic and metaphysics John Skorupski ENLIGHTENMENT AND ROMANTICISM IN MILL’S PHILOSOPHY Mill’s importance as one of the major figures of nineteenth century politics and culture, and the current interest in him as a moral and political… …   History of philosophy

  • formal logic — the branch of logic concerned exclusively with the principles of deductive reasoning and with the form rather than the content of propositions. [1855 60] * * * Introduction       the abstract study of propositions, statements, or assertively used …   Universalium

Share the article and excerpts

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