INCLUSION CRITERIA
An entry belongs in this subdivision if and only if its operators quantify over a temporal flow (next, until, always, since, eventually), interpreted over a structure that orders the instants or intervals of evaluation.
Required: At least one of the following:
- Tense or temporal operators (X, U, G, F, S) with a semantics over a linear or branching time order
- An interval-based temporal calculus with relations among periods
- A metric or real-time operator constraining the temporal distance between events
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).
Boundary: Real-time and hyperproperty logics (metric, signal, HyperLTL) live here; their use in verification is cross-listed with Applications/Verification. The modal mu-calculus and propositional dynamic logic appear here for their fixpoint/temporal reading and are cross-listed with Dynamic and Applications/Verification. Temporal epistemic systems are cross-listed with Epistemic.