Automated formal synthesis of provably safe digital controllers for continuous plants

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

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)223-244
Number of pages22
JournalActa Informatica
Volume57
Issue number1-2
Early online date6 Dec 2019
DOIs
Publication statusPublished - 1 Apr 2020

Fingerprint

Dive into the research topics of 'Automated formal synthesis of provably safe digital controllers for continuous plants'. Together they form a unique fingerprint.

Cite this