Automated formal synthesis of digital controllers for state-space physical plants
We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization...
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Conference item |
| Published: |
International Conference on Computer-Aided Verification
2017
|
| _version_ | 1797076712943517696 |
|---|---|
| author | Abate, A Bessa, I Cattaruzza, D Cordeiro, L David, C Kesseli, P Kroening, D Polgreen, E |
| author_facet | Abate, A Bessa, I Cattaruzza, D Cordeiro, L David, C Kesseli, P Kroening, D Polgreen, E |
| author_sort | Abate, A |
| collection | OXFORD |
| description | We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization of signals by the controller. Our approach has two stages, leveraging counterexample guided inductive synthesis (CEGIS) and reachability analysis. CEGIS synthesizes a static feedback controller that stabilizes the system under restrictions given by the safety of the reach space. Safety is verified either via BMC or abstract acceleration; if the verification step fails, we refine the controller by generalizing the counterexample. We synthesize stable and safe controllers for intricate physical plant models from the digital control literature. |
| first_indexed | 2024-03-07T00:07:40Z |
| format | Conference item |
| id | oxford-uuid:781ae09e-39f8-49d7-9345-fc14e0227f2e |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:07:40Z |
| publishDate | 2017 |
| publisher | International Conference on Computer-Aided Verification |
| record_format | dspace |
| spelling | oxford-uuid:781ae09e-39f8-49d7-9345-fc14e0227f2e2022-03-26T20:28:32ZAutomated formal synthesis of digital controllers for state-space physical plantsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:781ae09e-39f8-49d7-9345-fc14e0227f2eSymplectic Elements at OxfordInternational Conference on Computer-Aided Verification2017Abate, ABessa, ICattaruzza, DCordeiro, LDavid, CKesseli, PKroening, DPolgreen, EWe present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization of signals by the controller. Our approach has two stages, leveraging counterexample guided inductive synthesis (CEGIS) and reachability analysis. CEGIS synthesizes a static feedback controller that stabilizes the system under restrictions given by the safety of the reach space. Safety is verified either via BMC or abstract acceleration; if the verification step fails, we refine the controller by generalizing the counterexample. We synthesize stable and safe controllers for intricate physical plant models from the digital control literature. |
| spellingShingle | Abate, A Bessa, I Cattaruzza, D Cordeiro, L David, C Kesseli, P Kroening, D Polgreen, E Automated formal synthesis of digital controllers for state-space physical plants |
| title | Automated formal synthesis of digital controllers for state-space physical plants |
| title_full | Automated formal synthesis of digital controllers for state-space physical plants |
| title_fullStr | Automated formal synthesis of digital controllers for state-space physical plants |
| title_full_unstemmed | Automated formal synthesis of digital controllers for state-space physical plants |
| title_short | Automated formal synthesis of digital controllers for state-space physical plants |
| title_sort | automated formal synthesis of digital controllers for state space physical plants |
| work_keys_str_mv | AT abatea automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT bessai automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT cattaruzzad automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT cordeirol automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT davidc automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT kesselip automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT kroeningd automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants AT polgreene automatedformalsynthesisofdigitalcontrollersforstatespacephysicalplants |