Temporal logic

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am always hungry", "I will eventually be hungry", or "I will be hungry until I eat something"). It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.

Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems. For instance, one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously. Such a statement can conveniently be expressed in a temporal logic.

Motivation[edit]

Consider the statement "I am hungry". Though its meaning is constant in time, the statement's truth value can vary in time. Sometimes it is true, and sometimes false, but never simultaneously true and false. In a temporal logic, a statement can have a truth value that varies in time—in contrast with an atemporal logic, which applies only to statements whose truth values are constant in time. This treatment of truth-value over time differentiates temporal logic from computational verb logic.

Temporal logic always has the ability to reason about a timeline. So-called "linear-time" logics are restricted to this type of reasoning. Branching-time logics, however, can reason about multiple timelines. This permits in particular treatment of environments that may act unpredictably. To continue the example, in a branching-time logic we may state that "there is a possibility that I will stay hungry forever", and that "there is a possibility that eventually I am no longer hungry". If we do not know whether or not I will ever be fed, these statements can both be true.

first-order logic operators ‘¬’, ‘∧’, ‘∨’, ‘→’, ‘≡’, ‘∀’ and ‘∃’

realization operator U

functional symbol δ

propositional variables p₁,p₂,p₃,...

variables denoting time moments t₁,t₂,t₃,...

variables denoting time intervals n₁,n₂,n₃,...

P: "It was the case that..." (P stands for "past")

F: "It will be the case that..." (F stands for "future")

G: "It always will be the case that..."

H: "It always was the case that..."

operator R is sometimes denoted by V

The operator W is the weak until operator: $f\mathbf {W} g$ is equivalent to $f\mathbf {U} g\lor \mathbf {G} f$

Temporal logic has two kinds of operators: logical operators and modal operators.^[17] Logical operators are usual truth-functional operators ( $\neg ,\lor ,\land ,\rightarrow$ ). The modal operators used in linear temporal logic and computation tree logic are defined as follows.

Alternate symbols:

Unary operators are well-formed formulas whenever $B(φ)$ is well-formed. Binary operators are well-formed formulas whenever $B(φ)$ and $C(φ)$ are well-formed.

In some logics, some operators cannot be expressed. For example, N operator cannot be expressed in temporal logic of actions.

Some systems of

positional logic

(LTL) temporal logic without branching timelines

Linear temporal logic

(CTL) temporal logic with branching timelines

Computation tree logic

(ITL)

Interval temporal logic

(TLA)

Temporal logic of actions

(STL)^[18]

Signal temporal logic

(TTL)^[19]

Timestamp temporal logic

(PSL)

Property specification language

which generalizes LTL and CTL

CTL*

(HML)

Hennessy–Milner logic

which includes as a subset HML and CTL*

Modal μ-calculus

(MTL)^[20]

Metric temporal logic

(MITL)^[18]

Metric interval temporal logic

(TPTL)

Timed propositional temporal logic

(TLTL)^[21]

Truncated Linear Temporal Logic

(HyperLTL) ^[22]

Hyper temporal logic

Temporal logics include:

A variation, closely related to temporal or chronological or tense logics, are modal logics based upon "topology", "place", or "spatial position".^[23]^[24]

HPO formalism

Kripke structure

Automata theory

Chomsky grammar

State transition system

(DC)

Duration calculus

Hybrid logic

Temporal logic in finite-state verification

Reo Coordination Language

Modal logic

Research Materials: Max Planck Society Archive

Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: . POPL 1981: 164–176

The Temporal Logic of Branching Time

Amir Pnueli: FOCS 1977: 46–57

The Temporal Logic of Programs

Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

E. A. Emerson and Chin-Laung Lei, "", in Science of Computer Programming 8, pp. 275–306, 1987.

Modalities for model checking: branching time logic strikes back

E. A. Emerson, "", Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990

Temporal and modal logic

Cindy Eisner, Dana Fisman

A Practical Introduction to PSL

(2008). "From Church and Prior to PSL". In Orna Grumberg; Helmut Veith (eds.). 25 years of model checking: history, achievements, perspectives. Springer. ISBN 978-3-540-69849-4. preprint. Historical perspective on how seemingly disparate ideas came together in computer science and engineering. (The mention of Church in the title of this paper is a reference to a little-known 1957 paper, in which Church proposed a way to perform hardware verification.)

Vardi, Moshe Y.

Peter Øhrstrøm; Per F. V. Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence. Springer. 978-0-7923-3586-3.

ISBN

: "Temporal Logic"—by Anthony Galton.

Stanford Encyclopedia of Philosophy

by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)

Temporal Logic

by Ian Hodkinson, including a formal description of first-order temporal logic

Notes on games in temporal logic

CADP – provides generic model checkers for various temporal logic

is a powerful free model checker, LTL checker, simulator and refinement checker for CSP and its extensions (with shared variable, arrays, wide range of fairness).