Skip to main content

Automated formal synthesis of provably safe digital controllers for continuous plants

Alessandro Abate‚ Iury Bessa‚ Lucas Cordeiro‚ Cristina David‚ Pascal Kesseli‚ Daniel Kroening and Elizabeth Polgreen


We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as time-invariant models. Models are linear differential equations with inputs, evolving over a continuous state space. The synthesis precisely accounts for the effects of finite-precision arithmetic introduced by the controller. The approach uses counterexample-guided inductive synthesis: an inductive generalization phase produces a controller that is known to stabilize the model but that may not be safe for all initial conditions of the model. Safety is then verified via bounded model checking: if the verification step fails, a counterexample is provided to the inductive generalization, and the process further iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for physical plant models from the digital control literature.

Acta Informatica