Zum Inhalt springen

Temporale Logik der Aktionen

aus Wikipedia, der freien Enzyklopädie

Die Temporale Logik der Aktionen (TLA, {{#invoke:Vorlage:lang|full|CODE=en|SCRIPTING=Latn|SERVICE=englisch}}) wurde von Leslie Lamport entwickelt. Sie baut zum einen auf der Temporalen Logik (engl. {{#invoke:Vorlage:lang|flat}}) und zum anderen auf der Logik der Aktionen (engl. {{#invoke:Vorlage:lang|flat}}) 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

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.<ref>{{#if:|{{#iferror: {{#iferror:{{#invoke:Vorlage:FormatDate|Execute}}|}}| |}}}}{{#if:Krister Segerberg, John-Jules Meyer, Marcus Kracht, Edward N. Zalta|Krister Segerberg, John-Jules Meyer, Marcus Kracht, Edward N. Zalta: }}{{#if:|{{#if:The Logic of Action|[{{#invoke:Vorlage:Internetquelle|archivURL|1={{#invoke:URLutil|getNormalized|1={{{archiv-url}}}}}}} {{#invoke:Vorlage:Internetquelle|TitelFormat|titel=The Logic of Action}}]{{#if:| ({{{format}}})}}{{#if:| {{{titelerg}}}{{#invoke:Vorlage:Internetquelle|Endpunkt|titel={{{titelerg}}}}}}}}}|{{#if:https://plato.stanford.edu/archives/sum2020/entries/logic-action/%7C{{#if:{{#invoke:TemplUtl%7Cfaculty%7C}}%7C{{#invoke:Vorlage:Internetquelle%7CTitelFormat%7Ctitel={{#invoke:WLink%7CgetEscapedTitle%7C1=The Logic of Action}}}}|[{{#invoke:URLutil|getNormalized|1=https://plato.stanford.edu/archives/sum2020/entries/logic-action/}} {{#invoke:Vorlage:Internetquelle|TitelFormat|titel={{#invoke:WLink|getEscapedTitle|1=The Logic of Action}}}}]}}{{#if:| ({{{format}}}{{#if:The Stanford Encyclopedia of PhilosophyMetaphysics Research Lab, Stanford University2020{{#if: 2021-09-25 | {{#if:{{#invoke:TemplUtl|faculty|}}||1}}}} 

          | )
          | {{#if:{{#ifeq:en|de||{{#if:en|1}}}}| ; 
              | )}}}}}}{{#if:| {{{titelerg}}}{{#invoke:Vorlage:Internetquelle|Endpunkt|titel={{{titelerg}}}}}}}}}}}{{#if:https://plato.stanford.edu/archives/sum2020/entries/logic-action/%7C{{#if:{{#invoke:URLutil%7CisResourceURL%7C1=https://plato.stanford.edu/archives/sum2020/entries/logic-action/}}%7C%7C}}}}{{#if:The Logic of Action|{{#if:{{#invoke:WLink|isValidLinktext|1=The Logic of Action|lines=0}}||}}}}{{#if: The Stanford Encyclopedia of Philosophy| In: {{#invoke:Vorlage:Internetquelle|TitelFormat|titel=The Stanford Encyclopedia of Philosophy}}}}{{#if: Metaphysics Research Lab, Stanford University| Metaphysics Research Lab, Stanford University{{#if: 2020|,|{{#if: 2021-09-25 | {{#if:{{#invoke:TemplUtl|faculty|}}|;|,}}}}}}}}{{#if: 2020| {{#if:{{#invoke:DateTime|format|2020|noerror=1}}
            |{{#invoke:DateTime|format|2020|T._Monat JJJJ}}
            |{{#invoke:TemplUtl|failure|1=Fehler bei Vorlage:Internetquelle, datum=2020|class=Zitationswartung}} }}{{#if: |,|{{#if: 2021-09-25 | {{#if:{{#invoke:TemplUtl|faculty|}}|;|,}}}}}}}}{{#if: | S. {{{seiten}}}{{#if: |,|{{#if: 2021-09-25 | {{#if:{{#invoke:TemplUtl|faculty|}}|;|,}}}}}}}}{{#if: {{#invoke:TemplUtl|faculty|}}| {{#if:2020Metaphysics Research Lab, Stanford University|{{#if:|archiviert|ehemals}}|{{#if:|Archiviert|Ehemals}}}} {{#if:|vom|im}} Vorlage:Referrer{{#if:{{#invoke:TemplUtl|faculty|}}| (nicht mehr online verfügbar)}}{{#if: | am {{#iferror: {{#iferror:{{#invoke:Vorlage:FormatDate|Execute}}|}}|{{{archiv-datum}}}{{#if:502308||(?)}}}}}}{{#if: 2021-09-25|;}}}}{{#if: 2021-09-25| {{#if:2020Metaphysics Research Lab, Stanford University{{#invoke:TemplUtl|faculty|}}|abgerufen|Abgerufen}} {{#switch: {{#invoke:Str|len| {{#invoke:DateTime|format| 2021-09-25 |ISO|noerror=1}} }}
       |4=im Jahr
       |7=im
       |10=am
       |#default={{#invoke:TemplUtl|failure|1=Fehler bei Vorlage:Internetquelle, abruf=2021-09-25|class=Zitationswartung}} }} {{#invoke:DateTime|format|2021-09-25|T._Monat JJJJ}}
    | {{#invoke:TemplUtl|failure|1=Vorlage:Internetquelle | abruf=2026-MM-TT ist Pflichtparameter}} }}{{#if:{{#ifeq:en|de||{{#if:en|1}}}}|{{#if:The Stanford Encyclopedia of PhilosophyMetaphysics Research Lab, Stanford University2020{{#if: 2021-09-25 | {{#if:{{#invoke:TemplUtl|faculty|}}||1}}}}
       |  (
       | {{#if: | |  (}}
       }}{{#ifeq:{{#if:en|en|de}}|de||
          {{#invoke:Multilingual|format|en|slang=!|split=[%s,]+|shift=m|separator=, }}}}{{#if: |{{#ifeq:{{#if:en|en|de}}|de||, }}{{{kommentar}}}}})}}{{#if: 2020{{#if: 2021-09-25 | {{#if:{{#invoke:TemplUtl|faculty|}}||1}} }}en|{{#if: |: {{
 #if: 
 | „{{
     #ifeq: {{#if:{{#if: {{#invoke:templutl|faculty|}}|de-ch|de}}|{{#if: {{#invoke:templutl|faculty|}}|de-ch|de}}|de}} | de
     | Vorlage:Str trim
     | {{#invoke:Vorlage:lang|flat}}
     }}“
 | {{#ifeq: {{#if:{{#if: {{#invoke:templutl|faculty|}}|de-ch|de}}|{{#if: {{#invoke:templutl|faculty|}}|de-ch|de}}|de}} | de
     | „Vorlage:Str trim“
     | {{#invoke:Text|quote
         |1={{#if: 
              | {{#invoke:Vorlage:lang|flat}}
              | {{#invoke:Vorlage:lang|flat}} }}
         |2={{#if: {{#invoke:TemplUtl|faculty|}}|de-CH|de}}
         |3=1}} }}

}}{{#if: 

   |  (<templatestyles src="Person/styles.css" />{{#if:  | :  }}{{#if:  | , deutsch: „“ }})
   | {{#if: 
       |  ({{#if:  | , deutsch: „“ }})
       | {{#if:  |  (deutsch: „“) }}
 }}

}}{{#if: {{{zitat}}} 

   | {{#if: 
       | {{#if: {{{zitat}}}
           | Vorlage:": Text= und 1= gleichzeitig, bzw. Pipe zu viel }} }}
   | Vorlage:": Text= fehlt }}{{#if:  | {{#if: {{#invoke:Text|unstrip|{{{ref}}}}}
             | Vorlage:": Ungültiger Wert: ref=
             | {{{ref}}} }}

}}|.{{#if:{{#invoke:TemplUtl|faculty|}}|{{#if:||{{#ifeq: | JaKeinHinweis |{{#switch: 

   |0|=Vorlage:Toter Link/Core{{#if: https://plato.stanford.edu/archives/sum2020/entries/logic-action/
       | {{#if:  | [1] }} (Seite {{#switch:|no|0|=|dauerhaft }}nicht mehr abrufbar{{#if:  | , festgestellt im {{#invoke:DateTime|format||F Y}} }}. Suche im Internet Archive (T)){{#if: 
           | {{#if: deadurlausgeblendet | | Vorlage:Toter Link/archivebot }}
         }}
       |   (Seite {{#switch:|no|0|=|#default=dauerhaft }}nicht mehr abrufbar{{#if:  | , festgestellt im {{#invoke:DateTime|format||F Y}} }}.)
     }}{{#switch: 
         |no|0|=
         |#default={{#if:  ||  }}
    }}{{#invoke:TemplatePar|check
         |opt      = inline= url= text= datum= date= archivebot= bot= botlauf= fix-attempted= checked=
         |cat      = Wikipedia:Vorlagenfehler/Vorlage:Toter Link
         |errNS    = 0
         |template = Vorlage:Toter Link
         |format   = 
         |preview  = 1
    }}{{#if: https://plato.stanford.edu/archives/sum2020/entries/logic-action/
      | {{#if:{{#invoke:URLutil|isWebURL|https://plato.stanford.edu/archives/sum2020/entries/logic-action/}}
          || {{#if:  ||  }} 
        }}
      | {{#if: 
           | {{#if:  ||  }}
           | {{#if:  ||  }}
        }}
    }}{{#if: 
       | {{#if:{{#invoke:DateTime|format||F Y|noerror=1}}
             || {{#if:  ||  }} 
         }}
    }}{{#switch: deadurl
         |checked|deadurl|= 
         |#default=  {{#if:  ||  }}
    }}|#default= https://wiki-de.moshellshocker.dns64.de/index.php?title=Wikipedia:Defekte_Weblinks&dwl=https://plato.stanford.edu/archives/sum2020/entries/logic-action/ Die nachstehende Seite ist {{#switch:|no|0|=|dauerhaft }}nicht mehr abrufbar]{{#if:  | , festgestellt im {{#invoke:DateTime|format||F Y}} }}. (Suche im Internet Archive. (T).)  {{#if: 
            | {{#if: deadurlausgeblendet | | Vorlage:Toter Link/archivebot }}
         }}Vorlage:Toter Link/Core{{#switch: 
          |no|0|=
          |#default= {{#if:  ||  }}
        }}{{#invoke:TemplatePar|check
         |all      = inline= url=
         |opt      = datum= date= archivebot= bot= botlauf= fix-attempted= checked=
         |cat      = Wikipedia:Vorlagenfehler/Vorlage:Toter Link
         |errNS    = 0
         |template = Vorlage:Toter Link
         |format   = 
         |preview  = 1
       }}{{#if: https://plato.stanford.edu/archives/sum2020/entries/logic-action/
       | {{#if:{{#invoke:URLutil|isWebURL|https://plato.stanford.edu/archives/sum2020/entries/logic-action/}}
          || {{#if:  ||  }} 
        }}
    }}{{#if: 
         | {{#if:{{#invoke:DateTime|format||F Y|noerror=1}}
             || {{#if:  ||  }} 
           }}
    }}{{#switch: deadurl
         |checked|deadurl|= 
         |#default=  {{#if:  ||  }}
    }}[https://plato.stanford.edu/archives/sum2020/entries/logic-action/ }}|{{#switch: 
   |0|=Vorlage:Toter Link/Core{{#if: https://plato.stanford.edu/archives/sum2020/entries/logic-action/
       | {{#if:  | [2] }} (Seite {{#switch:|no|0|=|dauerhaft }}nicht mehr abrufbar{{#if:  | , festgestellt im {{#invoke:DateTime|format||F Y}} }}. Suche im Internet Archive (T)){{#if: 
           | {{#if:  | | Vorlage:Toter Link/archivebot }}
         }}
       |   (Seite {{#switch:|no|0|=|#default=dauerhaft }}nicht mehr abrufbar{{#if:  | , festgestellt im {{#invoke:DateTime|format||F Y}} }}.)
     }}{{#switch: 
         |no|0|=
         |#default={{#if:  ||  }}
    }}{{#invoke:TemplatePar|check
         |opt      = inline= url= text= datum= date= archivebot= bot= botlauf= fix-attempted= checked=
         |cat      = Wikipedia:Vorlagenfehler/Vorlage:Toter Link
         |errNS    = 0
         |template = Vorlage:Toter Link
         |format   = 
         |preview  = 1
    }}{{#if: https://plato.stanford.edu/archives/sum2020/entries/logic-action/
      | {{#if:{{#invoke:URLutil|isWebURL|https://plato.stanford.edu/archives/sum2020/entries/logic-action/}}
          || {{#if:  ||  }} 
        }}
      | {{#if: 
           | {{#if:  ||  }}
           | {{#if:  ||  }}
        }}
    }}{{#if: 
       | {{#if:{{#invoke:DateTime|format||F Y|noerror=1}}
             || {{#if:  ||  }} 
         }}
    }}{{#switch: 
         |checked|deadurl|= 
         |#default=  {{#if:  ||  }}
    }}|#default= https://wiki-de.moshellshocker.dns64.de/index.php?title=Wikipedia:Defekte_Weblinks&dwl=https://plato.stanford.edu/archives/sum2020/entries/logic-action/ Die nachstehende Seite ist {{#switch:|no|0|=|dauerhaft }}nicht mehr abrufbar]{{#if:  | , festgestellt im {{#invoke:DateTime|format||F Y}} }}. (Suche im Internet Archive. (T).)  {{#if: 
            | {{#if:  | | Vorlage:Toter Link/archivebot }}
         }}Vorlage:Toter Link/Core{{#switch: 
          |no|0|=
          |#default= {{#if:  ||  }}
        }}{{#invoke:TemplatePar|check
         |all      = inline= url=
         |opt      = datum= date= archivebot= bot= botlauf= fix-attempted= checked=
         |cat      = Wikipedia:Vorlagenfehler/Vorlage:Toter Link
         |errNS    = 0
         |template = Vorlage:Toter Link
         |format   = 
         |preview  = 1
       }}{{#if: https://plato.stanford.edu/archives/sum2020/entries/logic-action/
       | {{#if:{{#invoke:URLutil|isWebURL|https://plato.stanford.edu/archives/sum2020/entries/logic-action/}}
          || {{#if:  ||  }} 
        }}
    }}{{#if: 
         | {{#if:{{#invoke:DateTime|format||F Y|noerror=1}}
             || {{#if:  ||  }} 
           }}
    }}{{#switch: 
         |checked|deadurl|= 
         |#default=  {{#if:  ||  }}
    }}[https://plato.stanford.edu/archives/sum2020/entries/logic-action/ }} }}}}}}}}}}{{#if:|
        {{#invoke:Vorlage:Internetquelle|archivBot|stamp={{{archiv-bot}}}|text={{#if:|Vorlage:Webarchiv/archiv-bot}}

}}}}{{#invoke:TemplatePar|check |all= url= titel= |opt= autor= hrsg= format= sprache= titelerg= werk= seiten= datum= abruf= zugriff= abruf-verborgen= archiv-url= archiv-datum= archiv-bot= kommentar= zitat= AT= CH= offline= |cat= {{#ifeq: 0 | 0 | Wikipedia:Vorlagenfehler/Vorlage:Internetquelle}} |template= Vorlage:Internetquelle |format=0 |preview=1 }}</ref>

Notationsgrundlagen

  • Sei <math>F</math> ein syntaktisches Objekt, dann ist <math>F</math> seine semantische Bedeutung.
  • <math>\hat =</math> ist eine andere Schreibweise für <math>:=</math> und bedeutet „gleich per definitionem“.
  • <math>sv/v</math> bedeutet, dass <math>v</math> durch <math>sv</math> ersetzt wird.

Variablen, Werte und Zustände

Die Logik der Aktionen verwendet die folgenden drei Klassen:

<math>\textbf{Var}</math> – die Klasse aller Variablennamen
<math>\textbf{Val}</math> – die Klasse aller möglichen Werte für die Variablen (z. B. 10, „string“, <math>\operatorname{True}</math>)
<math>\textbf{St}</math> – die Klasse aller möglichen Zustände

Ein Zustand ist eine Abbildung <math>s\colon\textbf{Var}\to \textbf{Val}, x\mapsto s(x)</math>, das heißt, der Variablen <math>x</math> wird der Zustand <math>s(x)</math> zugewiesen. Die Zustände beschreiben die Semantik. Man verwendet <math>sx</math> statt <math>s(x)</math>. Mit <math>x</math> bezeichnet man somit die Abbildung <math>x\colon\textbf{St}\to \textbf{Val}</math>.

Somit ist die Schreibweise <math>sx</math> in polnischer Notation und bedeutet Anwendung von <math>s</math>.<ref>{{#invoke:Vorlage:Literatur|f}}</ref>

Zustandsfunktion

Eine Zustandsfunktion (engl. state function) ist ein nicht-boolescher Ausdruck aus Variablen und Konstanten, zum Beispiel <math>f := x^2 + y + 4</math>, dazu gehören auch Variablen <math>x</math> (da eine Variable als die Identitätsabbildung <math>x\mapsto x</math> interpretiert werden kann). Der Ausdruck <math>f</math> ist dann die Abbildung <math>f\colon\textbf{St}\to \textbf{Val}, s\mapsto sf</math>, das heißt, <math>f</math> oder <math>x^2 + y+4</math> ist eine Abbildung, die dem Zustand <math>s</math> den Wert <math>\left(sx\right)^2 + sy+4</math> zuordnet. Die Notation <math>sf</math> bezeichnet den Wert, den <math>f</math> dem Zustand <math>s</math> zuordnet.

Die semantische Definition von <math>sf</math> lautet<ref name="Lamport">{{#invoke:Vorlage:Literatur|f}}</ref>

<math>sf\ \hat = \ f(\forall v\colon sv/v)</math>.

Der Ausdruck <math>f(\forall v\colon sv/v)</math> bedeutet somit den Wert von <math>f</math>, wenn man alle <math>v</math> durch <math>sv</math> ersetzt.

Zusammenfassend:

Zustand <math>s</math> <math>\textbf{Var}\to \textbf{Val},x\mapsto s(x)=:sx</math>
Zustandsfunktion <math>f</math> <math>x^2+y+4</math>
Semantik <math>f</math> <math>\textbf{St}\to \textbf{Val},s\mapsto sf=(sx)^2+sy+4</math>

Zustandsprädikat

Ein boolescher Ausdruck <math>P</math> aus Variablen und Konstanten wird Zustandsprädikat (oder kurz Prädikat) genannt, ein Beispiel ist der Ausdruck <math>x=3+y</math>. Mit <math>P</math> bezeichnet man die Abbildung <math>P\colon\textbf{St}\to \operatorname{Booleans}</math> und <math>sP</math> ordnet entweder <math>\operatorname{True}</math> oder <math>\operatorname{False}</math> dem Zustand <math>s</math> zu. Wenn <math>sP=\operatorname{True}</math> gilt, dann sagt man <math>s</math> erfüllt das Prädikat <math>P</math>.<ref name="Lamport" />

Aktion und Schritte

Eine Aktion <math>\mathcal{A}</math> ist ein boolescher Ausdruck, der die Beziehung zwischen einem alten Zustand <math>s</math> und einem neuen Zustand <math>t</math> beschreibt. Die Aktion besteht aus „alten Variablen“ und „neuen Variablen“, wobei letztere mit einem <math>'</math> markiert sind. Zum Beispiel ist <math>x'+2=y</math> eine Aktion, die sagt, dass <math>y</math> im alten Zustand um <math>2</math> größer ist als <math>x</math> im neuen Zustand.

Der Ausdruck <math>[[\mathcal{A}]]</math> beschreibt die Beziehung zwischen zwei Zuständen, das heißt einen binären Operator, der den beiden Zuständen <math>s, t</math> einen booleschen Wert <math>s [[\mathcal{A}]] t</math> zuweist, dabei wird per definitionem links der alte Zustand und rechts der neue Zustand geschrieben. Die semantische Bedeutung <math>s [[\mathcal{A}]] t</math> von <math>\mathcal{A}</math> erhält man, indem man <math>v</math> durch <math>sv</math> und <math>v'</math> durch <math>tv</math> ersetzt. Ist <math>s[[\mathcal{A}]]t=\operatorname{True}</math>, dann nennt man <math>s, t</math> einen <math>\mathcal{A}</math>-Schritt (engl. <math>\mathcal{A}</math>-step).

Der Ausdruck <math>sy = x'+ 1t</math> bedeutet somit das Gleiche wie der boolesche Ausdruck <math>sy=tx+1</math>.

Die semantische Definition von <math>s[[\mathcal{A}]]t</math> lautet

<math>s[[\mathcal{A}]]t\ \hat = \ \mathcal{A}(\forall v\colon sv/v,\ tv/v')</math>.

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 <math>x</math> eine flexible Variable, dann besitzt die Aktion

<math>\exist m\in\mathbb{N}\colon mx'=n+x</math>

zwei rigide Variablen <math>m, n</math>, die nicht verändert werden.

Prädikat als Aktion

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

<math>F'\ \hat = \ F(\forall v\colon v'/v)</math>.

Des Weiteren ist <math>sP't</math> der gleiche Ausdruck wie <math>tP</math>, für alle Zustände <math>s, t</math>.

Beweisbarkeit und Gültigkeit

Eine Aktion <math>\mathcal{A}</math> ist gültig (engl. valid), geschrieben <math>\vDash \mathcal{A}</math> (siehe Tautologie), falls jeder Schritt ein <math>\mathcal{A}</math>-Schritt ist, das heißt also, <math>s[[\mathcal{A}]]t</math> ist <math>\operatorname{True}</math> für alle <math>s, t \in \textbf{St}</math>. Die semantische Definition lautet

<math>\vDash \mathcal{A}\ \hat = \ \forall s, t \in \textbf{St}\colon\ s[[\mathcal{A}]]t</math>

und für ein Prädikat <math>P</math>

<math>\vDash P\ \hat = \ \forall s \in \textbf{St}\colon \ sP</math>.

Ein Beispiel für eine gültige Aussage ist

<math>(x'+y\in \mathbb{N})\implies (x'+y \geq -x'+-y)</math>.

Beweisbare Formeln <math>F</math> werden wie in der mathematischen Logik mit <math>\vdash F</math> notiert (siehe Ableitung).

Enabled-Prädikate

Sei <math>\mathcal{A}</math> eine Aktion, dann ist <math>Enabled\ \mathcal{A}</math> ein Prädikat, das genau dann für einen Zustand wahr ist, falls es in dem Zustand möglich ist, einen <math>\mathcal{A}</math>-Schritt auszuführen. Die semantische Definition lautet<ref>{{#invoke:Vorlage:Literatur|f}}</ref>

<math>s[[Enabled\ \mathcal{A}]]\ \hat = \ \exist t \in \textbf{St}\colon s[[\mathcal{A}]]t</math>

für jeden Zustand <math>s</math>.

Temporale Logik

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.<ref>{{#invoke:Vorlage:Literatur|f}}</ref>

Temporale Formeln

Temporale Formeln bestehen aus elementaren Formeln sowie booleschen Operatoren und dem unären Operator <math>\square</math>, der „immer“ (engl. always) oder „global“ (engl. global) bedeutet. Mit <math>\sigmaF</math> wird der boolesche Ausdruck bezeichnet, den das <math>F</math> dem Verhalten <math>\sigma</math> zuweist. Mit <math>\langle s_0, s_1, \dots \rangle</math> wird das Verhalten bezeichnet, das im Zustand <math>s_0</math> beginnt. Man sagt <math>\sigma</math> erfüllt <math>F</math> genau dann, wenn <math>\sigmaF=\operatorname{True}</math>.

Da alle booleschen Ausdrücke durch <math>\wedge</math> und <math>\lnot</math> beschrieben werden können, genügt es, die Ausdrücke <math>\lnot F, F\wedge G</math> und <math>\square F</math> zu definieren. Die semantischen Definitionen sind somit<ref>{{#invoke:Vorlage:Literatur|f}}</ref>

<math>\sigma F \land G\ \hat = \ \sigma F \land \sigma G</math>
<math>\sigma \lnot F\ \hat = \ \lnot \sigma F</math>
<math>\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,</math>

wobei der erste Ausdruck bedeutet, dass ein Verhalten <math>F \land G</math> erfüllt, falls es beide Formeln <math>F</math> und <math>G</math> erfüllt. Der zweite Ausdruck bedeutet, dass das Verhalten <math>\lnot F</math> erfüllt, wenn es <math>F</math> nicht erfüllt. Die linke Seite des dritten Ausdruckes <math>\langle s_0, s_1, \dots\rangle \square F</math> bedeutet, dass die Formel <math>F</math> ab Zustand <math>s_0</math> gültig ist. Das heißt, die letzte Definition sagt, dass <math>F</math> immer gültig ist (da es per Induktionsschritt definiert ist).<ref name="Lamport" />

Schlussendlich-Operator

Die Formel <math>\lnot \square \lnot F</math> bedeutet, dass <math>F</math> nicht immer falsch ist und wird mit <math>\Diamond F</math> abgekürzt und schlussendlich (engl. eventually) genannt:

<math>\Diamond F\ \hat = \ \lnot \square \lnot F</math>

Die Formel <math>\Diamond \square F</math> bedeutet, dass <math>F</math> schlussendlich immer wahr ist.

Gültigkeit

Eine temporale Formel <math>F</math> ist gültig, falls jedes Verhalten die Formel erfüllt:

<math>\vDash F\ \hat = \ \forall \sigma \in \textbf{St}^{\infty}\colon \sigma F</math>

Temporale Logik der Aktionen

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 <math>\square</math>.

Ein einfaches Beispiel

Gegeben sei ein Algorithmus, der im Zustand <math>x=0</math> und <math>z=0</math> beginnt und dann nichtdeterministisch entweder <math>x</math> inkrementiert und <math>z</math> dekrementiert, oder umgekehrt. Als TLA würde das so aussehen:

<math>Init_{\phi}\ \hat = \ (x=0)\wedge (z=0)</math>
<math>\mathcal{A_1}\ \hat = \ (x'=x+1) \wedge (z'=z-1)</math>
<math>\mathcal{A_2}\ \hat = \ (x'=x-1) \wedge (z'=z+1)</math>
<math>\mathcal{A}\ \hat = \ \mathcal{A_1} \vee \mathcal{A_2}</math>
<math>\phi\ \hat = \ Init_{\phi} \wedge \square \mathcal{A}</math>

Dabei bezeichnet <math>\phi</math> eine Formel, <math>Init_{\phi}</math> den Initialzustand und <math>\mathcal{A}</math> eine Aktion.

Stotternde Schritte

Als stotternde Schritte (engl. stuttering steps) werden Schritte bezeichnet, die das Programm pausieren. In dem Beispiel oben würde das bedeuten, dass <math>x</math> und <math>z</math> nicht verändert werden. Ein solcher Schritt lässt sich zum Beispiel so implementieren:<ref>{{#invoke:Vorlage:Literatur|f}}</ref>

<math>Init_{\phi}\ \hat = \ (x=0)\wedge (z=0)</math>
<math>\mathcal{A_1}\ \hat = \ (x'=x+1) \wedge (z'=z-1)</math>
<math>\mathcal{A_2}\ \hat = \ (x'=x-1) \wedge (z'=z+1)</math>
<math>\mathcal{S_1}\ \hat = \ (x'=x) \wedge (z'=z)</math>
<math>\mathcal{A}\ \hat = \ \mathcal{A_1} \vee \mathcal{A_2}</math>
<math>\phi\ \hat = \ Init_{\phi} \wedge \square (\mathcal{A} \vee \mathcal{S_1})</math>

Um stotternde Schritte einfach zu beschreiben, führt man weitere Notationen ein. Mit der Notation <math>\langle x', z'\rangle = \langle x, z\rangle</math> wird <math>(x'=x)\wedge (z'=z)</math> bezeichnet und statt <math>\langle x', z'\rangle</math> zu schreiben, notiert man einfach <math>\langle x, z\rangle'</math>. Für eine Zustandsfunktion <math>f</math> und eine Aktion <math>\mathcal{A}</math> definieren wir:

<math>[\mathcal{A}]_{f} \ \hat = \ \mathcal{A}\vee (f'=f)</math>

Dann bedeutet <math>[\mathcal{M}]_{\langle x, z\rangle}</math> somit:

<math>[\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}</math>

Somit lassen sich die beiden Zeilen

<math>\mathcal{S_1}\ \hat = \ (x'=x) \wedge (z'=z)</math>
<math>\phi\ \hat = \ Init_{\phi} \wedge \square (\mathcal{A} \vee \mathcal{S_1})</math>

vereinfachen zu

<math>\phi\ \hat = \ Init_{\phi} \wedge \square [\mathcal{A}]_{\langle x, z \rangle}</math>.

Syntax und Semantik

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

<math>{[\mathcal{A} ]}_f</math> <math>\hat =</math> <math>\mathcal{A} \lor ( f' = f )</math>
<math>{\langle \mathcal{A} \rangle}_f </math> <math>\hat =</math> <math>\mathcal{A} \land ( f' \neq f ),</math>

wobei <math>\mathcal{A}</math> eine Aktion ist, <math>f</math> eine Zustandsfunktion ist und durch Anwendung logischer Gesetze <math>(\mathcal{A}\wedge (f'\neq f)) = \lnot(\lnot\mathcal{A}\vee (f'=f))</math> gilt.

Für die Formel-Syntax gilt:

<math>\langle Formel \rangle</math>

<math>\hat =</math>

<math> \langle Formel \rangle \land \langle Formel \rangle </math> <math>\vert</math> <math> \langle Formel \rangle \lor \langle Formel \rangle </math> <math>\vert</math> <math> \neg \langle Formel \rangle </math> <math>\vert</math> <math> \Box \langle Formel \rangle </math> <math>\vert</math> <math> \Diamond \langle Formel \rangle </math> <math>\vert</math> <math> \langle Pr\ddot adikat \rangle </math> <math>\vert</math> <math> \Box {\lbrack Aktion \rbrack}_{\langle f \rangle} </math> <math>\vert</math> <math> \Box {\langle Aktion \rangle}_{\langle f \rangle} </math>

Das Symbol <math>|</math> ist als Trennungszeichen zu verstehen.

Verhaltenseigenschaften

Eine Sicherheitseigenschaft (engl. safety property) garantiert, dass unerwünschte Zustände nicht passieren. Zum Beispiel ist der durch <math>Init_{\phi}</math> spezifizierte Start eine Sicherheitseigenschaft.

Eine Lebendigkeitseigenschaft (engl. liveness property) garantiert, dass erwünschte Zustände erreicht werden, was mit dem <math>\Diamond \square \mathcal{A}</math> formuliert werden kann. Möchte man eine Fairness und dass zwei Eigenschaften unendlich Mal wiederholt werden, so verwendet man stattdessen <math>\Diamond \square \mathcal{A}_1 \wedge \Diamond \square \mathcal{A}_2</math>. Somit würde man im obigen Beispiel Folgendes erhalten:

<math>\phi\ \hat = \ Init_{\phi} \wedge \square [\mathcal{A}]_{\langle x, z \rangle} \wedge \Diamond \square \mathcal{A}_1 \wedge \Diamond \square \mathcal{A}_2</math>

Schwache und starke Fairness

In einem nebenläufigen System unterscheidet man zwischen schwacher und starker Fairness.

Schwache Fairness <math>\operatorname{WF}</math> (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 <math>\operatorname{SF}</math> (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

Literatur

  • 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

      | {{#ifeq: 20160415185024 | *
    | Vorlage:Webarchiv/Wartung/Stern{{#if: Temporal Logic of Action. | {{#invoke:WLink|getEscapedTitle|Temporal Logic of Action.}} | {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}} }} (Archivversionen)
    | {{#iferror: {{#time: j. F Y|20160415185024}}
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/DatumDer Wert des Parameters {{#if: wayback | wayback | Datum }} muss ein gültiger Zeitstempel der Form YYYYMMDDHHMMSS sein!
         | {{#if: Temporal Logic of Action. | {{#invoke:WLink|getEscapedTitle|Temporal Logic of Action.}} | {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y|20160415185024}} im Internet Archive{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
      }}
  }}
      | {{#if:
          | {{#iferror: {{#time: j. F Y|{{{webciteID}}}}}
    | {{#switch: {{#invoke:Str|len|{{{webciteID}}}}}
       | 16= {{#if: Temporal Logic of Action. | {{#invoke:WLink|getEscapedTitle|Temporal Logic of Action.}} | {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{{webciteID}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | 9 = {{#if: Temporal Logic of Action. | {{#invoke:WLink|getEscapedTitle|Temporal Logic of Action.}} | {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{#invoke:Expr|base62|{{{webciteID}}}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | #default= Der Wert des Parameters {{#if: webciteID | webciteID | ID }} muss entweder ein Zeitstempel der Form YYYYMMDDHHMMSS oder ein Schüsselwert mit 9 Zeichen oder eine 16-stellige Zahl sein!Vorlage:Webarchiv/Wartung/webcitation{{#if:  || }}
      }}
    | c|{{{webciteID}}}}} {{#if: Temporal Logic of Action. | {{#invoke:WLink|getEscapedTitle|Temporal Logic of Action.}} | {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}} }} (Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y|{{{webciteID}}}}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
  }}
          | {{#if: 
              | Vorlage:Webarchiv/Today
              | {{#if:
                      | Vorlage:Webarchiv/Generisch
                      | {{#if: Temporal Logic of Action. | {{#invoke:WLink|getEscapedTitle|Temporal Logic of Action.}} | {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}} }}  
                 }}}}}}}}{{#if:
    | Vorlage:Webarchiv/archiv-bot
  }}{{#invoke:TemplatePar|check
     |all      = url=
     |opt      = text= wayback= webciteID= archive-is= archive-today= archiv-url= archiv-datum= ()= archiv-bot= format= original=
     |cat      = Wikipedia:Vorlagenfehler/Vorlage:Webarchiv
     |errNS    = 0
     |template = Vorlage:Webarchiv
     |format   = *
     |preview  = 1
  }}{{#ifexpr: {{#if:20160415185024|1|0}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}} <> 1
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Genau einer der Parameter 'wayback', 'webciteID', 'archive-today', 'archive-is' oder 'archiv-url' muss angegeben werden.|1}}
  }}{{#if: 
    | {{#switch: {{#invoke:Webarchiv|getdomain|{{{archiv-url}}}}}
        | web.archive.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von Internet Archive erkannt, bitte Parameter 'wayback' benutzen.|1}} 
        | webcitation.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von WebCite erkannt, bitte Parameter 'webciteID' benutzen.|1}} 
        | archive.today |archive.is |archive.ph |archive.fo |archive.li |archive.md |archive.vn = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von archive.today erkannt, bitte Parameter 'archive-today' benutzen.|1}}
      }}{{#if: 
         | {{#iferror: {{#iferror:{{#invoke:Vorlage:FormatDate|Execute}}|}}
             | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Wert des Parameter 'archiv-datum' ist ungültig oder hat ein ungültiges Format.|1}}
          |  }} 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Pflichtparameter 'archiv-datum' wurde nicht angegeben.|1}}
      }}
    | {{#if: 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Parameter 'archiv-datum' ist nur in Verbindung mit 'archiv-url' angebbar.|1}}
      }}
  }}{{#if:{{#invoke:URLutil|isHostPathResource|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf}}
    || {{#if:  || }}
  }}{{#if: Temporal Logic of Action.
    | {{#if: {{#invoke:WLink|isBracketedLink|Temporal Logic of Action.}}
        | {{#if:  || }}
      }}
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Linktext_fehlt
  }}{{#switch: 
    |addlarchives|addlpages= {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/Parameter}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: enWP-Wert im Parameter 'format'.|1}}
  }}{{#ifeq: {{#invoke:Str|find|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf%7Carchiv}} |-1
    || {{#ifeq: {{#invoke:Str|find|{{#invoke:Str|cropleft|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf%7C4}}%7Chttp}} |-1
         || {{#switch: {{#invoke:Webarchiv|getdomain|http://www4.informatik.tu-muenchen.de/lehre/seminare/ps/WS0203/desaster/Ulmer-TemporalLogicOfActions-Ausarbeitung-13-01-03.pdf }}
              | abendblatt.de | daserste.ndr.de | inarchive.com | webcitation.org = 
              | #default = {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/URL}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Archiv-URL im Parameter 'url' anstatt URL der Originalquelle. Entferne den vor der Original-URL stehenden Mementobestandteil und setze den Archivierungszeitstempel in den Parameter 'wayback', 'webciteID', 'archive.today' oder 'archive-is' ein, sofern nicht bereits befüllt.|1}}
            }} 
       }}
  }}. (PDF; 413 kB). Proseminar-Ausarbeitung, TU München.

Einzelnachweise

<references />

Abgerufen von „https://wiki-de.moshellshocker.dns64.de/index.php?title=Temporale_Logik_der_Aktionen&oldid=502308“