Since their invention in 1958, implantable pacemakers have revolutionized the treatment of cardiac diseases, significantly enhancing patient quality of life. With each subsequent generation, advances in miniaturization of electronics, batteries, and sensors have facilitated smaller, more capable pacemakers. These innovations have brought faster arrhythmia detection and introduced novel therapies, but they also come with challenges. Tailoring these complex therapies to individual patients often requires the expertise of highly skilled cardiac clinicians, leaving many patients with suboptimal care based on generalized models. Moreover, increasing device complexity extends development and verification times, delaying the availability of new therapies. Despite these challenges, patient safety remains paramount.

Recent advances in reinforcement learning (RL) offer promising solutions to address these challenges. RL has demonstrated the ability to discover innovative solutions to complex problems at scale. Applied to pacemaker design, RL offer a transformative paradigm for managing complexity, reducing development time, and enabling personalized therapies, all while upholding the highest safety standards. Through RL’s scalable exploration capabilities, new therapies can be discovered, and existing ones can be tailored to meet individual patient needs. However, the safe application of RL hinges on the precise construction of the reward mechanisms---often expressed as finite-state machines known as reward machines---that guide the behavior of RL agents. Errors in defining these learning objectives can result in flawed training and incorrect system operation.

This dissertation addresses the critical problem of rigorously and unambiguously expressing the requirements for cardiac pacemakers in a form that can be effectively processed by RL algorithms. Formal logic provides a robust framework for specifying system behaviors, and automated methods for translating these requirements into reward machines can significantly enhance the reliability of RL-based system design. A key contribution of this dissertation is the formalization of cardiac pacemaker requirements using a real-time formal logic called Duration Calculus (DC). We further explore techniques to translate these formal specifications into reward machines, ensuring that RL algorithms trained to maximize these rewards produce strategies that satisfy the original requirements.

While formal logic offers a precise method for defining RL learning objectives, the manual process of capturing requirements in this format is often labor-intensive and error-prone. To address this, the dissertation investigates the potential of AI technologies---such as recurrent neural networks and large language models---to extract formal logic and reward machines from expert demonstrations provided by skilled cardiac clinicians.

RL's exploratory nature can lead it to make incorrect actions leading to grave consequences. To enhance safety, we also develop approaches to restrict the choices available to RL agents using safety shields derived from formal requirements. These shields ensure that the strategies generated by RL algorithms comply with critical safety and performance criteria.

By integrating formal logic, reinforcement learning, and cutting-edge AI techniques, this dissertation establishes a robust foundation for the next generation of intelligent cardiac pacemaker design, while ensuring both safety and personalization.