Interval Temporal Logic

Origin. 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.

Models. Time as intervals, not points. Point-based: things happen at moments. Interval-based: things happen over durations. Relations between intervals: before, during, overlaps, etc. Modal operators access related intervals.

Formalism.

Allen's 13 relations: For intervals i, j:

before/after: i ends before j starts
meets/met-by: i ends where j starts
overlaps/overlapped-by: partial intersection
during/contains: i within j
starts/started-by: share start
finishes/finished-by: share end
equals: same interval

Halpern-Shoham (HS) logic: Six modal operators (and inverses):

⟨B⟩φ: φ holds at some beginning subinterval
⟨E⟩φ: φ holds at some ending subinterval
⟨D⟩φ: φ holds at some proper subinterval (during)
⟨A⟩φ: φ holds at some meeting interval (after)
⟨L⟩φ: φ holds at some later interval
⟨O⟩φ: φ holds at some overlapping interval

Plus inverses: B̄, Ē, D̄, Ā, L̄, Ō

Semantics: M, [a,b] ⊨ ⟨B⟩φ iff ∃c ∈ [a,b). M, [a,c] ⊨ φ

Duration Calculus (DC): Extends ITL with integration. ∫P — duration of P over interval. ∫P ≤ k: P holds for at most k time.

Symbols.

Symbol	Unicode	Name	Meaning
⟨B⟩	—	Begins	Beginning subinterval
⟨E⟩	—	Ends	Ending subinterval
⟨D⟩	—	During	Proper subinterval
⟨A⟩	—	After	Adjacent later
⟨L⟩	—	Later	Strictly later
⟨O⟩	—	Overlaps	Overlapping
∫	U+222B	Integral	Duration of a state over an interval
[a,b]	—	Interval	Time interval
⟨·⟩	—	Angle brackets	Existential interval modality
B̄	U+0042, U+0304	B with combining macron	Inverse of an interval relation
⊨	U+22A8	Satisfaction	Truth at an interval of a model
∃	U+2203	Exists	Existential clause of the semantics
∈	U+2208	Membership	Endpoint drawn from the interval

Metatheory. Halpern and Shoham (1991) proved the validity problem for HS undecidable over every standard class of interval structures — all linear orders, all discrete orders, all dense orders, and each of ℕ, ℤ, ℚ, ℝ — by a reduction from the halting problem for Turing machines, so the logic is undecidable at its point of definition rather than through some optional extension. The standard translation sends HS into first-order logic over the underlying order with two free variables, the interval [a,b] being the pair a ≤ b, which places its expressiveness below full first-order logic over the order. Decidability of the fragments is delicate rather than graded: BE, with ⟨B⟩ and ⟨E⟩ together, is already undecidable (Lodaya 2000), while BB̄, with ⟨B⟩ and its inverse, is NP-complete and the neighborhood fragment AĀ is NEXPTIME-complete. The classification of the 2¹² HS fragments was completed by Bresolin, Della Monica, Goranko, Montanari, and Sciavicco.

Applies to. Planning (activities have durations). Real-time systems (timing constraints). Workflow and process modeling. Medical protocols. Music representation. Animation and multimedia. Temporal databases with intervals.

Limitations. Undecidability is the default and decidability the exception: the full logic is undecidable over every standard class of orders, and the boundary runs between fragments in ways no syntactic measure predicts, so a specification must be written inside a chosen fragment and cannot be strengthened without rechecking whether the fragment is still decidable. Over ℕ the validity problem is not recursively enumerable, so no finitary axiomatization is complete there. The logic is purely qualitative — it orders and nests intervals but says nothing about their length — and the metric repair, Duration Calculus, is undecidable in full. Intervals are primitive, so there is no next-instant operator and no way to project a proposition onto points without an added homogeneity assumption, which itself shifts the decidability boundary rather than leaving it fixed.