Automated formal synthesis of provably safe digital controllers for continuous plants

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)