Temporal Logics

Summary

Goranko’s Cambridge Elements volume is a compact survey of temporal logics from Prior’s tense logic through linear-time, branching-time, first-order, interval, hybrid, metric, epistemic, and application-oriented variants. It treats temporal logic as a family of systems distinguished by models of time, temporal operators, and formal semantics rather than as a single monolithic logic.

For this wiki, the main value is foundational: it places Linear Temporal Logic and CTL-style branching logics inside a broader semantic landscape. It also gives precise anchors for why temporal-logic choices matter in verification, AI representation, natural-language semantics, and strategic or nondeterministic reasoning.

Key Claims

• Temporal logics differ along three axes: ontological assumptions about time, the operators used to compose temporalized formulas, and the semantic clauses used to define truth and consequence.
• Instant-based time frames T = <T, prec> can be linear, dense, discrete, unbounded, or forward-branching; each choice changes which temporal principles are valid.
• Prior’s basic tense logic uses past/future operators P, F, H, and G, with Kripke-style semantics over instants and a precedence relation.
• Linear-time temporal logics are appropriate when executions are treated as single traces; LTL over N uses X and U as standard primitives and is central for specifying infinite computations.
• Branching-time temporal logics model nondeterministic possible futures. Peircean semantics evaluates future claims at instants over all histories, while Ockhamist semantics evaluates formulas on (history, instant) branches.
• First-order temporal logic adds object quantification to temporal operators, making domain variation, identity through time, and Barcan-style quantifier/temporal interactions technically important.
• Applications in computer science and AI rely on the same semantic distinctions: safety, liveness, fairness, model checking, planning, temporal databases, action reasoning, and temporal natural-language interpretation each favor different fragments or model assumptions.

Methods / Formalism

• Instant-based temporal frames are structures T = <T, prec> with instants and a precedence relation. A linear frame satisfies trichotomy; a forward-branching frame is backward-linear, so the past is fixed while the future can branch.
• Prior’s tense logic defines formulas from atomic propositions, Boolean connectives, and weak past/future operators:

$$\varphi ::=p\mid \perp \mid \neg \varphi \mid (\varphi \wedge \varphi )\mid P\varphi \mid F\varphi .$$

The strong operators are duals: H phi := not P not phi and G phi := not F not phi.

• In tense models M = <T, prec, V>, M,t |= P phi iff phi is true at some earlier instant, and M,t |= F phi iff phi is true at some later instant.
• LTL over N uses future operators X and U:

$$\sigma ,i\models X\varphi ⟺\sigma ,i+1\models \varphi ,$$ $$\sigma ,i\models \varphi U\psi ⟺\exists j\ge i.\sigma ,j\models \psi \wedge \forall k(i\le k<j\Rightarrow \sigma ,k\models \varphi ).$$

The derived operators are F phi := top U phi and G phi := not F not phi.

• Branching-time structures are trees whose histories are maximal linear paths. Branching-Time Semantics records the Peircean and Ockhamist clauses in detail.
• First-order temporal models add a global domain, local domains Dom_t, and time-indexed interpretations of predicates and constants. Presentist/varying-domain and eternalist/constant-domain semantics differ on principles such as temporal Barcan formulas.

Evidence / Experiments

• This is a survey and teaching text rather than an empirical paper. Its evidence is definitional, proof-theoretic, and bibliographic: semantic clauses, axiom schemes, expressiveness results, decidability notes, and references across philosophy, computer science, AI, and linguistics.
• The text reviews standard results such as Kamp’s expressive-completeness theorem for Since/Until over Dedekind-complete strict linear orders, decidability of LTL, decidability of Peircean branching-time validity, and the automata-theoretic role of Buchi and Rabin results in temporal-logic decision methods.

Connections

• Extends Linear Temporal Logic by locating LTL as the discrete linear-time fragment of a larger family of Prior-style and Kamp-style temporal logics.
• Seeds Branching-Time Temporal Logic and Branching-Time Semantics for CTL, CTL*, Peircean, and Ockhamist semantics.
• Complements Hofmann2025 - Automata Theory and Logic: Hofmann and Lange emphasize automata/logic decision procedures, while Goranko emphasizes semantic varieties of time and temporal operators.
• Gives background for Probabilistic Strategic Timed CTL and Alternating-Time Temporal Logic, where branching futures are combined with probabilities, real-time bounds, or coalition strategies.
• Connects to Duration Calculus and interval temporal logics because Goranko contrasts instant-based semantics with interval-based models for duration and progressive events.
• Supports Formal Methods and Temporal Logic as a navigational foundation for choosing between trace logics, branching logics, interval logics, and first-order temporal languages.

Open Questions

• Should the wiki split out separate concept pages for first-order temporal logic, CTL/CTL*, and interval temporal logic once later sources use them directly?
• Which safe-RL and MARL notes currently say “temporal logic” when they specifically mean linear-time trace semantics?
• When should branching-time semantics in the wiki be represented as path quantification, strategic ability, or probability over paths?

Citation

Goranko, V. (2023). Temporal Logics. Cambridge Elements in Philosophy and Logic. Cambridge University Press. https://doi.org/10.1017/9781009170093