Temporal logic

Temporal logics or time logics are extensions of the logic, can be detected by the temporal sequences. There are applications of modal logic, based on a before-after relationship between time points. Whether this result is a dense or continuous time order, depends on the determination of this relation.

General

The philosophical foundations of temporal logics were developed by Arthur Norman Prior and John McTaggart. The two main model families from time logics are linear temporal logic ( LTL) and Computation Tree Logic (CTL ). LTL while extending from a linear sequence of points in time, describes a branching CTL timing. Because both logics can describe different situations, but also have a large intersection, we define CTL * of which both CTL, as well as LTL, a subset are.

A -temporal logic such as propositional logic can statements whose truth values ​​change with time, do not treat or only with difficulty adequately. So is " It's Raining " true when it at the place and time of the utterance raining, otherwise not. Therefore Classical -temporal logics include the time of utterance to the truth conditions ( A case of " It is raining " is uttered at a particular time and is true if it rains at this time). Each case of the utterance of the sentence thus has its own truth conditions. In contrast, lead time logics a modal operators, so that each case of the utterance of the sentence is subject to the same truth- conditions. These operators allow it to analyze more sophisticated temporal statements logically, so that " It was raining ", " It is raining ", " It 's still raining " truth-functional on the performance of " It's Raining " depending on certain times.

The computer Amir Pnueli has the temporal logic introduced into the test systematics of large and complex computer systems and thus described reproducible and comparable conditions in programs and thus test criteria.

In the dialogical logic of a frame rule for a temporal logic is introduced so that an early dialog match statement made will no longer be available later in the dialog.