# Correct-by-construction control synthesis for buck converters with event-triggered state measurement

## TL;DR

This paper presents a novel correct-by-construction switching controller for buck converters using event-triggered measurements, addressing challenges of outdated state information with a belief space abstraction and demonstrating effectiveness through simulation.

## Contribution

Introduces a new control synthesis method that accounts for out-of-date measurements via belief space abstraction for power converters.

## Key findings

- Controller effectively manages outdated measurements.
- Belief space abstraction preserves key properties.
- Simulation confirms improved control performance.

## Abstract

In this paper, we illustrate a new correct-by-construction switching controller for a power converter with event-triggered measurements. The event-triggered measurement scheme is beneficial for high frequency power converters because it requires relatively low-speed sampling hardware and is immune to unmodeled switching transients. While providing guarantees on the closed-loop system behavior is crucial in this application, off-the-shelf abstraction-based techniques cannot be directly employed to synthesize a controller in this setting because controller cannot always get instantaneous access to the current state. As a result, the switching action has to be based on slightly out-of-date measurements. To tackle this challenge, we introduce the out-of-date measurement as an extra state variable and project out the inaccessible real state to construct a belief space abstraction. The properties preserved by this belief space abstraction are analyzed. Finally, an abstraction-based synthesis method is applied to this abstraction. We demonstrate the controller on a constant on-time buck voltage regulator plant with an event-triggered sampler. The simulation verifies the effectiveness of our controller.