Rechargeable Lithium(Li)-Ion Batteries are a ubiquitous element of modern technology, as they pertain to efficient and sustainable energy storage for Electric Vehicles (EVs), as well as wind and solar farms. In the last decades, the production and design of such batteries and their adjacent embedded control, charging, and safety protocols, denoted by Battery Management Systems (BMS), has taken centre stage in the energy transition. A fundamental challenge to be addressed in battery technology, however, is the trade-off between the speed of the charging protocol employed by the BMS and the aging behaviour exhibited by the battery resulting in the loss of capacity in the battery cell, all while maintaining the safe operation of the battery.

This thesis aims to explore electrochemical models describing the charging and aging behaviour of Li-Ion Battery Systems, as well as the current existing charging protocols that aim to maximize charging speed while minimizing the aging effects that result in capacity loss. The proposed approach in this thesis is to adopt a data-driven approach to controller design, implementing improvements on an existent Reinforcement Learning (RL) pipeline to design an aging-aware battery-charging protocol, and extending the work into the field of Formal Methods for Systems and Control. This is done by expressing the closed-loop system resulting from a trained charging policy in the form of a data-driven abstraction capable of verifying the formal system specifications under probabilistic guarantees. Furthermore, a Counterexample-Guided Inductive Synthesis (CEGIS) scheme is proposed to additionally guide the training of the charging policy based on information from the learning results.