• README ⤓ .txt 2026-07-17T121634.146 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-07-17T120407.600 000000000000856
  Allen (1983). Interval relations. Qualitative time. Constraint reasoning. Foundation of temporal AI.
• Arabic Post-Avicennan ⤓ .md 2026-07-15T081754.000 000000000017144
  12th-15th centuries. Al-Rāzī, al-Khūnajī, al-Kātibī, al-Taftāzānī. Refined modal-temporal syllogistic. Shamsiyya tradition. Foundation for later Islamic logic.
• Avicenna Temporal ⤓ .md 2026-07-15T081629.000 000000000018320
  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-07-17T120407.600 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-07-15T060903.000 000000000020224
  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.
• CTL Star ⤓ .md 2026-07-17T120407.600 000000000000736
  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-07-15T070919.000 000000000014784
  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-07-15T072004.000 000000000014792
  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-07-16T001655.000 000000000034368
  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; Clouston, Bizjak, Grathwohl, and Birkedal (2015) added clocks for productivity.
• Hybrid Logic ⤓ .md 2026-07-15T054121.000 000000000029176
  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-07-15T061938.000 000000000019224
  Clarkson, Finkbeiner, Koleini, Kuz, Rabe introduced HyperLTL (2014). Temporal logic for hyperproperties. Extends LTL with trace quantifiers. Express information flow, observational determinism. Model checking hyperproperties.
• Interval Temporal Logic ⤓ .md 2026-07-15T060705.000 000000000021152
  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-07-15T060902.000 000000000019448
  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-07-15T070913.000 000000000014648
  Koymans (1990). Temporal logic with real-time constraints. Bounded temporal operators. Decidable over timed words. Foundation for real-time verification.
• Modal Mu-Calculus ⤓ .md 2026-07-17T120407.600 000000000000848
  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-07-15T072000.000 000000000014880
  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-07-15T062130.000 000000000017776
  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-07-17T120407.600 000000000000880
  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.
• Signal Temporal Logic ⤓ .md 2026-07-15T070916.000 000000000014608
  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-07-15T063303.000 000000000018216
  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-07-15T060311.000 000000000023328
  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-07-15T052403.000 000000000026736
  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, Allen Emerson, and Joseph Sifakis developed Computation Tree Logic (CTL) and model checking.
• Temporal-Logic-Verification ⤓ .md 2026-07-15T052403.000 000000000026736
  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, Allen Emerson, and Joseph Sifakis developed Computation Tree Logic (CTL) and model checking.
• Tense Logic ⤓ .md 2026-07-15T060505.000 000000000020448
  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).
• CRITERIA ⤓ .txt 2026-07-17T120407.600 000000000000744
  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).