Temporal logic

clyde — Mon, 15 Jan 2007 10:55:53 +0800

Any logic which uses the existential quantifier or the universal quantifier is said to be a first-order logic. Any logic which views time as a sequence of states is a temporal logic, and any logic which uses only two truth values is a binary logic.
temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time.

Consider the statement: "I am hungry." Though its meaning is constant in time. In fact, the truth value of the statement can vary in time.

In a temporal logic, statements can have a truth value which can vary in time. we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry until I eat something".

Temporal logic has two kinds of operators: logical operators and modal operators. Logical operators are usual truth-functional operators. The modal operators used in Linear Temporal Logic and Computation Tree Logic are
U(until), X(next), F(finally), G(golbally), A(all) , E(exists) ...etc.

Temporal logics include

CTL*, which includes as a subset
1. Computation Tree Logic (CTL)
2. Linear temporal logic (LTL)
3. Interval temporal logic (ITL)
4. μ calculus

資料來源：http://en.wikipedia.org/wiki/Temporal_logic