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
∫	U+222B	Integral	Duration of a state over the interval
ℓ	U+2113	Length	Interval length, equal to ∫1
;	—	Chop	Split the interval into two adjacent parts
⌈ ⌉	U+2308, U+2309	Ceiling brackets	⌈P⌉: P holds almost everywhere on a nonpoint interval
⌈⌉	—	Point interval	The interval has length zero
◇	U+25C7	Somewhere	Holds on some subinterval
□	U+25A1	Everywhere	Holds on every subinterval
≤	U+2264	Less or equal	Bound on a duration or length
⊨	U+22A8	Satisfaction	Truth at an interval [b,e]
∃	U+2203	Exists	Chop point in the semantics of ;

Metatheory. Duration Calculus is Moszkowski's interval temporal logic — the chop operator and its associated proof rules — extended with the duration terms ∫P, and the standard proof system is relatively complete with respect to that base rather than complete outright. The semantics presupposes finite variability: on any bounded interval a state function changes value finitely often, which is what makes ∫P a well-defined Riemann integral. Zhou Chaochen, Hansen, and Sestoft (STACS 1993) drew the decidability boundary. The restricted calculus RDC, in which duration terms occur only through ⌈P⌉ and no ∫P is compared with a constant, has decidable satisfiability over both discrete and continuous time, the discrete case by translation into regular languages, at non-elementary cost. Full Duration Calculus, with ∫P compared against constants, is undecidable. Between the two, linear duration invariants — inequalities Σ cᵢ∫Pᵢ ≤ k — can be checked against timed automata by linear programming.

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

Limitations. The duration terms that give the calculus its point are exactly what makes it undecidable, and the decidable fragment RDC, which drops them, is decidable only at non-elementary cost. The proof system is relatively complete with respect to interval temporal logic, not complete on its own, so a failed derivation locates no defect in the specification. Finite variability is an assumption of the semantics rather than a theorem about systems: a state function that switches infinitely often on a bounded interval — Zeno behaviour, exactly what a real-time analysis would want to rule out — falls outside the models, so the calculus cannot be used to exclude it. Because ⌈P⌉ says only that P holds almost everywhere, the logic is blind to sets of measure zero and can express nothing about instantaneous events. Chop is sequential; there is no parallel composition, so concurrent components are not combined within the calculus.