# Duration Calculus

**Origin.** Zhou Chaochen, Hoare, Ravn (1991). Interval temporal logic with durations. Integral of state over interval. Real-time system specification. Foundation for embedded systems.

**Models.** State durations as integrals. ∫P: duration P holds in interval. Chop operator for interval composition. Specify timing constraints declaratively.

**Formalism.**

*States and durations:*
P: state expression (0 or 1 valued)
∫P: duration of P in current interval
∫P = ∫[b,e] P(t) dt for interval [b,e]

*Interval operators:*
ℓ: length of interval (ℓ = ∫1)
⌈P⌉: P holds almost everywhere (∫P = ℓ ∧ ℓ > 0)
⌈⌉: point interval (ℓ = 0)

*Chop operator:*
φ ; ψ: interval splits into φ-part then ψ-part
[b,e] ⊨ φ ; ψ iff ∃m. [b,m] ⊨ φ and [m,e] ⊨ ψ

*Example specifications:*
□(⌈gas ∧ ¬flame⌉ → ℓ ≤ 4)
"Gas without flame for at most 4 seconds"

□(⌈request⌉ ; ⌈¬grant⌉ ; ⌈grant⌉ → ∫¬grant ≤ 5)
"Response within 5 seconds"

*Derived operators:*
◇φ = true ; φ ; true
□φ = ¬◇¬φ

*Extensions:*
Mean value: ∫P/ℓ
Probability: probabilistic DC
Higher-order: quantify over states

**Symbols.**

| Symbol | Unicode | Name | Meaning |
|--------|---------|------|---------|
| ∫P | U+222B | Integral | Duration of P |
| ℓ | — | Length | Interval length |
| ; | — | Chop | Sequential composition |
| ⌈P⌉ | — | Almost everywhere | P holds |

**Metatheory.** Undecidable in general. Decidable fragments (DC without chop). Model checking approaches. Refinement calculus.

**Applies to.** Real-time systems. Embedded controllers. Railway signaling. Gas burner control. Safety-critical systems.

**Limitations.** Undecidable. Specifications can be complex. Gap between spec and implementation. Verification challenging.

© 2026 Lingenic LLC