Duration Calculus

Definition

Duration Calculus is an interval temporal logic for specifying real-time properties over timed traces, especially constraints involving how long a condition holds within an interval. A technical anchor is the duration constraint

$$\int P\bowtie c,$$

which compares the accumulated time for which proposition P holds against constant c.

Why It Matters

Many cyber-physical requirements are not just about event order. They also ask how long a signal holds, whether a timer window has elapsed, or whether accumulated exposure stays below a bound. Duration Calculus gives a compact language for such requirements, and bounded fragments can sometimes be compiled into executable automata for monitoring, verification, synthesis, or shielding.

Formalism / Key Objects

• A timed trace is a sequence (s_0,tau_0)...(s_n,tau_n) where each s_i is a set of propositions and each tau_i is a timestamp.
• Formulae are interpreted over intervals [b,e] of the timed trace.
• Useful constructs include interval length ell bowtie c, accumulated duration integral P bowtie c, counting-style constraints, Boolean connectives, and chop D1 ; D2 for interval decomposition.
• In bounded semantics, formulae are evaluated over traces of fixed finite length. This can make automata construction and reachability checks decidable for fragments that would be difficult or undecidable in the unrestricted setting.
• Duration Calculus Pacemaker Shields records the bounded DC to stopwatch-automata to RL-shield pipeline from Dole et al.

Connections

• Temporal Logic is the parent specification area; DC adds direct duration-measurement operators.
• Runtime Verification can use executable DC-derived automata as monitors.
• Safety Games arise when controllable and uncontrollable signals are separated.
• Shielding can use the resulting safe region to block learner actions that would violate real-time requirements.
• Control Theory matters when DC specifications constrain embodied closed-loop timing, as in pacemaker-heart systems.

Common Confusions

• Duration Calculus is not just LTL with clocks; the accumulated-duration modality is the central extra expressivity.
• Full DC can have undecidable decision problems, so bounded or otherwise restricted fragments matter.
• Compiling a requirement into an automaton does not by itself prove the original informal requirement was complete or clinically adequate.

Key Sources

• Dole2023 - Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements