README⤓ .txt 2026-10-22T165042.936 000000000000728 Logics whose operators quantify over a flow of time—"next," "until," "always," "since," "eventually"—interpreted over structures that order the points or intervals of evaluation. The temporal reading of the modality is what distinguishes these systems: accessibility is the passage of time.
Allen Interval Calculus⤓ .md 2026-10-22T180154.561 000000000000856 Allen (1983). Interval relations. Qualitative time. Constraint reasoning. Foundation of temporal AI.
Arabic Post-Avicennan⤓ .md 2026-08-20T023902.000 000000000052760 The twelfth to fifteenth centuries, working from Avicenna rather than from Aristotle. Fakhr al-Dīn al-Rāzī (d. 1210) reopened the Avicennan modal syllogistic critically; Afḍal al-Dīn al-Khūnajī (d. 1248) rebuilt it in the Kashf al-asrār; Najm al-Dīn al-Kātibī al-Qazwīnī (d. 1276) compressed the result into al-Risāla al-Shamsiyya, which became the standard madrasa handbook and drew the commentary of Quṭb al-Dīn al-Rāzī al-Taḥtānī (d. 1365) and the glosses of Sa'd al-Dīn al-Taftāzānī (d. 1390) and al-Sayyid al-Sharīf al-Jurjānī (d. 1413). The commentary-and-gloss form carried the system into the Ottoman, Persian, and Indian traditions and kept it in teaching use into the nineteenth century.
Avicenna Temporal⤓ .md 2026-08-20T023447.000 000000000039784 Ibn Sīnā/Avicenna (980-1037). Al-Shifā, Al-Ishārāt. Temporal reading of modality. Absolute vs conditional necessity. Extended Aristotelian syllogistic. Foundation of Arabic modal logic.
Buchi Automata⤓ .md 2026-10-22T180154.561 000000000000872 J. Richard Büchi, "On a decision method in restricted second order arithmetic" (1962), which introduced ω-automata to prove S1S decidable; Rabin (1969) extended it to trees and S2S; McNaughton (1966) gave the determinization. Vardi and Wolper's "An automata-theoretic approach to automatic program verification" (1986) turned the theorem into the technology every model checker runs on.
Computation Tree Logic⤓ .md 2026-10-22T091825.000 000000000032912 Clarke and Emerson introduced CTL (1981). Branching time: tree of possible futures. Path quantifiers + temporal operators. Foundation for symbolic model checking. CTL* combines CTL and LTL. Tools: SMV, NuSMV; UPPAAL checks a timed-CTL subset over timed automata.
CTL Star⤓ .md 2026-10-22T084914.000 000000000035904 Emerson and Halpern (1986), "Sometimes and Not Never Revisited." The logic that subsumes both CTL and LTL by freely combining path quantifiers with linear temporal operators, resolving the expressiveness dispute between branching- and linear-time schools.
Duration Calculus⤓ .md 2026-08-20T021919.000 000000000032552 Zhou Chaochen, Hoare, Ravn (1991). Interval temporal logic with durations. Integral of state over interval. Real-time system specification. Foundation for embedded systems.
Freeze Quantifiers⤓ .md 2026-08-20T021540.000 000000000031256 Alur and Henzinger (1994). Freeze current time/value. Compare across positions. Real-time and data constraints. First-order temporal with data.
Guarded Recursion⤓ .md 2026-10-22T180154.561 000000000000896 Hiroshi Nakano, "A modality for recursion" (LICS 2000), which introduced the later modality ▷ and its fixed-point combinator; Appel, Melliès, Richards, and Vouillon's "very modal model" (2007) connected it to step-indexing; Birkedal, Møgelberg, Schwinghammer, and Støvring's topos of trees (2011) gave the canonical model; Atkey and McBride (2013) added clocks for productivity.
Halpern-Shoham Logic⤓ .md Interval Temporal Logic.md 000000000000208 Halpern and Shoham introduced HS (1991). Allen's interval algebra (1983). Logic where time intervals are primitive, not points. Duration matters, not just ordering. Natural for reasoning about processes and activities.
Hybrid Logic⤓ .md 2026-10-22T165042.936 000000000000760 Arthur Prior introduced nominals for temporal logic (1967). Modern hybrid logic developed by Patrick Blackburn and colleagues (1990s-2000s). Extends modal logic with explicit reference to worlds/states. Bridges modal and first-order logic while maintaining modal decidability. Useful for temporal databases, spatial reasoning, and description logics.
HyperLTL⤓ .md 2026-08-20T014507.000 000000000033616 Clarkson, Finkbeiner, Koleini, Micinski, Rabe, and Sánchez introduced HyperLTL (POST 2014). Temporal logic for hyperproperties. Extends LTL with trace quantifiers. Express information flow, observational determinism. Model checking hyperproperties.
Interval Temporal Logic⤓ .md 2026-10-22T091834.000 000000000034992 Halpern and Shoham introduced HS (1991). Allen's interval algebra (1983). Logic where time intervals are primitive, not points. Duration matters, not just ordering. Natural for reasoning about processes and activities.
Linear Temporal Logic⤓ .md 2026-10-22T091817.000 000000000032096 Pnueli introduced LTL for program verification (1977). Temporal operators over infinite sequences. Linear time: one future path. Foundation for model checking (Vardi, Wolper). Tools: SPIN, NuSMV, SPOT. Turing Award to Pnueli (1996).
Metric Temporal Logic⤓ .md 2026-10-22T165042.936 000000000000840 Ron Koymans, "Specifying real-time properties with metric temporal logic" (Real-Time Systems, 1990). LTL says that a response eventually follows a request but not that it follows within five milliseconds; MTL supplies the missing quantity by decorating each temporal operator with an interval of the time domain. It grew up alongside the timed automata of Alur and Dill (1994), which give the operational counterpart, and its decidable core was isolated by Alur, Feder, and Henzinger (1996) under the slogan "the benefits of relaxing punctuality."
Modal Mu-Calculus⤓ .md 2026-08-20T030722.000 000000000049264 Dana Scott and Jaco de Bakker used fixed points in program semantics (1969); Park (1969, 1976) on fixpoint induction. Dexter Kozen, "Results on the propositional μ-calculus" (1983), gave the system and its axiomatization; Walukiewicz (1995) proved completeness. The modal mu-calculus combines modal logic with fixed-point operators. Subsumes CTL, LTL, PDL in expressive power. Foundation for model checking algorithms (OBDD-based, game-based).
Past Temporal Logic⤓ .md 2026-10-22T165042.936 000000000000824 Kamp (1968), Lichtenstein et al. (1985). Temporal operators for the past. Since dual to until. Expressively equivalent to future-only (on ω-words). Succinctness advantages.
Probabilistic CTL⤓ .md 2026-10-22T165042.936 000000000000808 Hansson and Jonsson introduced PCTL (1994). Extends CTL with probability bounds. Properties of probabilistic systems (DTMCs, MDPs). Foundation for PRISM model checker. Workhorse of probabilistic verification.
Propositional Dynamic Logic⤓ .md 2026-08-20T032946.000 000000000039128 Fischer and Ladner introduced PDL (1979). Modal logic of programs. Combines propositional logic with regular expressions over actions. Foundation for program verification. Decidable fragment of dynamic logic.
Rabin Tree Theorem⤓ .md 2026-10-22T180154.561 000000000000816 Michael O. Rabin, "Decidability of second-order theories and automata on infinite trees" (announced Bulletin of the AMS 1968; full proof Transactions of the AMS 141, 1969, 1–35): S2S, the monadic second-order theory of the infinite binary tree, is decidable. The proof invented automata on infinite trees, and its hardest step was the complementation lemma, which Rabin proved by transfinite induction. Yuri Gurevich and Leo Harrington, "Trees, automata, and games" (STOC 1982), reproved the lemma by the forgetful determinacy of infinite games; Andrey Muchnik gave a proof avoiding transfinite induction (published in Russian in 1984, circulated through Alexei Semenov's lectures, written out in full by Igor Walukiewicz); E. Allen Emerson and Charanjit Jutla, "Tree automata, mu-calculus and determinacy" (FOCS 1991), recast it through parity acceptance and memoryless determinacy, the form the field now uses.
Signal Temporal Logic⤓ .md 2026-08-20T021112.000 000000000032192 Maler and Nickovic (2004). Temporal logic over real-valued signals. Predicates on continuous values. Quantitative semantics: robustness. Foundation for CPS verification.
Temporal Description Logic⤓ .md 2026-08-20T022231.000 000000000032096 Artale, Franconi, Schild, and others (1990s-2000s). Combines description logic with temporal logic. Concepts change over time. Temporal operators on concepts and roles. Ontologies with temporal dimension. Foundation for temporal knowledge representation.
Temporal Logic of Actions⤓ .md 2026-10-22T090714.000 000000000036928 Leslie Lamport developed TLA (1994) and TLA+ (1999). Combines temporal logic with actions (state transitions). Specification language for concurrent and distributed systems. Used at Amazon, Microsoft, and others for system design. TLC model checker and TLAPS proof system.
Temporal Logic⤓ .md 2026-10-22T085733.000 000000000036920 Arthur Prior developed tense logic (1957, 1967), applying modal logic to time. Amir Pnueli (1977) introduced Linear Temporal Logic (LTL) for program verification, winning the Turing Award for this work. Edmund Clarke and Allen Emerson developed Computation Tree Logic (CTL) and model checking; Joseph Sifakis, with Jean-Pierre Queille, developed model checking independently.
Tense Logic⤓ .md 2026-10-22T090936.000 000000000034328 Prior introduced tense logic (1957, 1967). Time as modal operators: past and future. P (it was the case), F (it will be the case). Philosophically motivated: McTaggart's A-series. Foundation for temporal logic in CS (linear time).
Timed Automata⤓ .md 2026-10-22T180154.561 000000000000872 Rajeev Alur and David Dill, "Automata for modeling real-time systems" (ICALP 1990), in journal form "A theory of timed automata" (Theoretical Computer Science 126, 1994, 183–235): finite automata over infinite words augmented with real-valued clocks, guards comparing clocks to constants, and resets. The companion logic is TCTL: Rajeev Alur, Costas Courcoubetis, and David Dill, "Model-checking in dense real-time" (Information and Computation 104, 1993, 2–34). David Dill, "Timing assumptions and verification of finite-state concurrent systems" (CAV 1989), supplied the zone and difference-bound-matrix machinery the implementations run on.
CRITERIA⤓ .txt 2026-07-15T161841.000 000000000008992 Not sufficient: Action or program execution as the modality (Dynamic). Knowledge or belief over time absent a genuine temporal operator (Epistemic). Obligation (Deontic). Bare alethic necessity (Alethic).