Duration Calculus Pacemaker Shields
Context
Dole2023 - Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements uses bounded Duration Calculus requirements for a dual-chamber pacemaker, compiles them into stopwatch automata, solves the induced safety game, and uses the safe action region as a shield around an adaptive RL controller.
Formal Statement
For a bounded DC formula D over a finite timed trace length n, construct an automaton A_D^[0,n] that accepts exactly the bounded timed traces satisfying D. For duration constraints, a stopwatch variable accumulates the time spent in states satisfying the proposition:
When controllable pacemaker outputs and uncontrollable heart/environment signals are separated, the compiled automaton induces a safety game. Solving the game yields a safe region W; a shield permits an RL action only when the resulting controlled transition remains in W.
Derivation / Construction
- Formalize pacemaker timing requirements in bounded Duration Calculus.
- Build automata inductively for subformulae and bounded intervals.
- For duration formulae, add a stopwatch that runs exactly while the relevant proposition holds and check the comparison at the accepting transition.
- For chop formulae, concatenate component automata over split intervals.
- Use acyclicity of the bounded construction to encode reachability/satisfiability as quantifier-free linear real arithmetic.
- Partition signals into controllable and uncontrollable components, then solve the resulting safety game with a controllable-predecessor computation.
- Wrap the RL controller with the resulting maximally permissive action set.
Implications
The construction gives a useful pattern for safe adaptation in real-time systems: retain a formal non-negotiable safety envelope while allowing learning inside the permitted region. Its strength depends on the adequacy of the formal requirements, the bounded-fragment assumption, and the fidelity of the simulated or deployed heart/environment model.