Temporale Logik

Temporale Logiken oder Zeitlogiken sind Erweiterungen der Logik, durch die zeitliche Abläufe erfasst werden können. Es handelt sich um Anwendungen der Modallogik, die auf einer Vorher-Nachher-Beziehung zwischen Zeitpunkten basieren. Ob daraus eine dichte oder diskrete Zeitordnung entsteht, ist von der Bestimmung dieser Relation abhängig.

Allgemeines

Die philosophischen Grundlagen temporaler Logiken wurden von Arthur Norman Prior und John McTaggart entwickelt. Die beiden wichtigsten Modellfamilien von Zeitlogiken sind die Lineare temporale Logik (LTL) und Computation Tree Logic (CTL). Während LTL von einer linearen Abfolge von Zeitpunkten ausgeht, beschreibt CTL eine verzweigende Zeitfolge. Weil beide Logiken verschiedene Sachverhalte beschreiben können, aber auch eine große Schnittmenge haben, definiert man CTL* von welchen sowohl CTL, wie auch LTL, eine Teilmenge sind.

Eine atemporale Logik wie die Aussagenlogik kann Aussagen, deren Wahrheitswerte sich mit der Zeit ändern, nicht oder nur mit Mühe adäquat behandeln. So ist „Es regnet“ nur wahr, wenn es am Ort und zur Zeit der Äußerung gerade regnet, sonst nicht. Klassische atemporale Logiken zählen daher den Äußerungszeitpunkt zu den Wahrheitsbedingungen (Ein Fall von „Es regnet“ wird zu einem bestimmten Zeitpunkt geäußert und ist wahr, wenn es zu diesem Zeitpunkt regnet). Jeder Fall der Äußerung des Satzes hat somit eigene Wahrheitsbedingungen. Hingegen führen Zeitlogiken modale Operatoren ein, so dass jeder Fall der Äußerung des Satzes unter denselben Wahrheitsbedingungen steht. Diese Operatoren lassen es zu, differenziertere zeitliche Aussagen logisch zu analysieren, so dass „Es hat geregnet“, „Es wird regnen“, „Es regnet immer“ wahrheitsfunktional von der Erfüllung von „Es regnet“ zu bestimmten Zeitpunkten abhängig ist.

Der Informatiker Amir Pnueli hat die temporale Logik in die Testsystematiken von großen und komplexen EDV-Systemen eingeführt und damit reproduzierbare und vergleichbare Zustände in Programmen und damit Testkriterien beschrieben. Beim Auftreten von Parallelitäten wie in vielen Systemen der Informatik ist der zeitliche Ablauf von entscheidender Bedeutung und muss in der Beschreibung logischer Systeme berücksichtigt werden. Der Turing-Preisträger Leslie Lamport entwickelte sowohl für Hardware- als auch für Software-Systeme die Temporale Logik der Aktionen (TLA).

In der dialogischen Logik wird eine Rahmenregel für eine zeitliche Logik so eingeführt, dass eine früh im Dialogspiel gemachte Aussage später im Dialog nicht mehr zur Verfügung steht.

Literatur

Philosophie:

  • Arthur Prior: Time and Modality. Oxford University Press 1957
  • dieselben: Temporal Logic. From Ancient Ideas to Artificial Intelligence, Springer 1995
  • John McTaggart Ellis McTaggart: The Unreality of Time. In: Mind. A Quarterly Review of Psychology and Philosophy 17/1908, S. 457–474. (Deutsche Übersetzung: Die Irrealität der Zeit. In: Walther Ch. Zimmerli u. Mike Sandbothe: Klassiker der modernen Zeitphilosophie. Wissenschaftliche Buchgesellschaft, Darmstadt 1993, S. 67–86).
  • Per Øhrstrøm, Per F.V.Hasle: Modern temporal logic: the philosophical background, in: Dov Gabbay, John Woods (Hrsg.): Handbook of the History of Logic, Band 7, Elsevier 2006, S. 447–498
  • Edmund Runggaldier: Formal semantische Erneuerung der Metaphysik. In: Matthias Lutz-Bachmann (Hg.): Metaphysik heute - Probleme und Perspektiven der Ontologie. Alber, Freiburg 2007, S. 57 (67–72) („Kontinuanten und Zeit“, „Zeitlogik und das Problem des Jetzt“, „A- und B-Serien“ (John McTaggart Ellis McTaggart)).

Informatik:

  • Jürgen Dassow: Logik für Informatiker. Vieweg&Teubner 2005, ISBN 3519005182, S. 125ff
  • Dov M. Gabbay, Ian Hodkinson, Mark Reynolds: Temporal Logic: Mathematical Foundations and Computational Aspects, Band 1, Oxford UP 1994
  • Dov M. Gabbay, Mark A. Reynolds, Marcelo Finger: Temporal Logic - Mathematical Foundations and Computational Aspects, Band 2, Clarendon Press Oxford 2000; ISBN 0-19-853768-9
  • Stéphane Demri, Valentin Goranko, Martin Lange: Temporal Logic in Computer Science: Finite State Systems, Cambridge UP 2016

Siehe auch

Weblinks