Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants
This work addresses the challenge of automating the design of correct-by-construction digital controllers for control engineers, reducing manual effort and errors.
The paper presents a new algorithm for automatically synthesizing digital stabilizing controllers for continuous plants, accounting for time discretization, quantization, and finite-precision arithmetic. The tool DSSynth generates stable controllers for intricate plant models within minutes.
Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counter-example guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.