Temporale Logik
# 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

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.
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 und Computation Tree Logic, die sich darin unterscheiden, ob sie eine geschlossene Zeitlinie annehmen oder Verzweigungen zulassen. Eine Verallgemeinerung der beiden Logiken wird als CTL* bezeichnet.
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.
Amir Pnueli gelang die Anwendung der temporalen Logik in der Informatik. Sein Aufsatz The Temporal Logic of Programs von 1977 löste einen Paradigmenwechsel in der Untersuchung des dynamischen Verhaltens von Computersystemen aus. Seine Analyse des Laufzeitverhaltens von parallelen und seriellen Computerprogrammen mit formallogischen Mitteln ermöglichte den Umgang mit Parallelität, für die zeitliche Ablauf von Computerprogrammen von entscheidender Bedeutung ist. Leslie Lamport adaptierte Pnuelis temporale Logik für Programme sowohl für Hardware- als auch für Software-Systeme adaptiert als Temporale Logik der Aktionen.