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

Abstract

A common cardiac arrhythmia, known as heart block or AV block, is a condition where the electrical signal con- As the complexity of artificial pacemakers continues to grow, trolling the ventricular contractions are partially or com- the importance of capturing its functional correctness re- pletely blocked (Vijayaraman and Ellenbogen 2017). De- quirement formally cannot be overestimated. The pacemaker system specification document by Boston Scientific provides pending upon the severity of this block, pacemaker therapy a widely accepted set of specifications for pacemakers. As may be indicated. A pacemaker is an implantable electronic these specifications are written in a natural language, they device that sends electrical impulses to the heart to regu- are not amenable to automated verification, synthesis, or late the heartbeat. The correctness of the pacemaker-heart reinforcement learning of pacemaker systems. This paper closed-loop system is time-critical: it should not only pro- presents a formalization of these requirements for a dual- vide supportive pacing when needed, it must ensure that the chamber pacemaker in duration calculus (DC), a highly ex- heart is not sent into unnaturally fast heart beats. Further- pressive real-time specification language. The proposed for- more, there are secondary requirements to improve the qual- malization allows us to automatically translate pacemaker re- ity of life such as detecting and supplying increased rates quirements into executable specifications as stopwatch au- when the patient exercises (rate-adaptive pacing) and maxi- tomata, which can be used to enable simulation, monitoring, validation, verification and automatic synthesis of pacemaker mizing battery longevity (2.2% risk of infection; 0.4% mor- systems. The cyclic nature of the pacemaker-heart closed- tality rate per pacemaker replacement (Polyzos, Konstan- loop system results in DC requirements that compile to a de- telias, and Falagas 2015