Abstract
We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as linear, time-invariant models. The synthesis accounts for errors caused by the digitization effects introduced by digital controllers operating in either fixed- or floating-point arithmetic. Our approach uses counterexample-guided inductive synthesis (CEGIS): in the first phase an inductive generalisation engine produces a possible solution that is safe for some possible initial conditions but may not be safe for all initial conditions. Safety for all initial conditions is then verified in a second phase either via bounded model checking or abstract acceleration; if the verification step fails, a counterexample is provided to the inductive generalisation and the process iterates until a safe controller is obtained. We implemented our approach in a tool named DSSynth (Digital-System Synthesizer) and demonstrate its practical value by automatically synthesizing safe controllers for physical plant models from the digital control literature.
Original language | English |
---|---|
Number of pages | 2 |
Publication status | Published - 18 May 2018 |
Event | Seventh Workshop on Synthesis - Oxford, United Kingdom Duration: 18 Jul 2018 → 18 Jul 2018 http://synt2018.seas.ucla.edu/index.html |
Workshop
Workshop | Seventh Workshop on Synthesis |
---|---|
Abbreviated title | SYNT 2018 |
Country/Territory | United Kingdom |
City | Oxford |
Period | 18/07/18 → 18/07/18 |
Internet address |