Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements Conference Proceeding uri icon



  • As the complexity of pacemaker devices continues to grow, the importance of capturing its functional correctness requirement formally cannot be overestimated. The pacemaker system specification document by emph{Boston Scientific} provides a widely accepted set of specifications for pacemakers. ; As these specifications are written in a natural language, they are not amenable for automated verification, synthesis, or reinforcement learning of pacemaker systems. This paper presents a formalization of these requirements for a dual-chamber pacemaker in emph{duration calculus} (DC), a highly expressive real-time specification language.; The proposed formalization allows us to automatically translate pacemaker requirements into executable specifications as stopwatch automata, which can be used to enable simulation, monitoring, validation, verification and automatic synthesis of pacemaker systems. ; The cyclic nature of the pacemaker-heart closed-loop system results in DC requirements that compile to a decidable subclass of stopwatch automata. We present shield reinforcement learning (shield RL), a shield synthesis based reinforcement learning algorithm, by automatically constructing safety envelopes from DC specifications.

publication date

  • February 7, 2023

has restriction

  • gold

Date in CU Experts

  • February 2, 2024 12:22 PM

Full Author List

  • Dole K; Gupta A; Komp J; Krishna S; Trivedi A

author count

  • 5

Other Profiles

International Standard Serial Number (ISSN)

  • 2159-5399

Electronic International Standard Serial Number (EISSN)

  • 2374-3468

Additional Document Info

start page

  • 14792

end page

  • 14800


  • 37


  • 12