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.