Repository logo

Automated formal synthesis of provably safe digital controllers for continuous plants

Published version

Change log


Abstract: 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.



Original Article

Journal Title

Acta Informatica

Conference Name

Journal ISSN


Volume Title



Springer Berlin Heidelberg
Engineering and Physical Sciences Research Council (EP/J012564/1)
European Research Council (280053)
H2020 Future and Emerging Technologies (280053)