TEMPORAL LOGIC
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.
Entries are organized by the model of time and the granularity of its operators. Linear systems (LTL, tense, past, HyperLTL) fix a single future; branching systems (CTL, CTL*, the modal mu-calculus) quantify over paths through a tree. Point-based systems are set against interval systems (Allen's calculus, interval temporal logic, duration calculus). Qualitative operators are set against metric and real-time ones (metric and signal temporal logic, freeze quantifiers). Further entries treat temporal reasoning about action and programs (temporal logic of actions, propositional dynamic logic), probabilistic time (probabilistic CTL), hybrid reference to instants, verification uses, and historical sources (Avicenna, post-Avicennan Arabic).