Sound and automated synthesis of digital stabilizing controllers for continuous plants
Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counterexample guided inductive synthesis that automates the design of digital controllers that are correct by construction. The syn...
| Main Authors: | , , , , , , |
|---|---|
| Format: | Conference item |
| Published: |
Association for Computing Machinery
2017
|
| _version_ | 1797082621881090048 |
|---|---|
| author | Abate, A Bessa, I Cattaruzza, D Cordeiro, L David, C Kesseli, P Kroening, D |
| author_facet | Abate, A Bessa, I Cattaruzza, D Cordeiro, L David, C Kesseli, P Kroening, D |
| author_sort | Abate, A |
| collection | OXFORD |
| description | Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counterexample guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes. |
| first_indexed | 2024-03-07T01:30:19Z |
| format | Conference item |
| id | oxford-uuid:9362b4bf-6535-4db0-92fa-3d634ea6e651 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:30:19Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:9362b4bf-6535-4db0-92fa-3d634ea6e6512022-03-26T23:31:52ZSound and automated synthesis of digital stabilizing controllers for continuous plantsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:9362b4bf-6535-4db0-92fa-3d634ea6e651Symplectic Elements at OxfordAssociation for Computing Machinery2017Abate, ABessa, ICattaruzza, DCordeiro, LDavid, CKesseli, PKroening, DModern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counterexample guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes. |
| spellingShingle | Abate, A Bessa, I Cattaruzza, D Cordeiro, L David, C Kesseli, P Kroening, D Sound and automated synthesis of digital stabilizing controllers for continuous plants |
| title | Sound and automated synthesis of digital stabilizing controllers for continuous plants |
| title_full | Sound and automated synthesis of digital stabilizing controllers for continuous plants |
| title_fullStr | Sound and automated synthesis of digital stabilizing controllers for continuous plants |
| title_full_unstemmed | Sound and automated synthesis of digital stabilizing controllers for continuous plants |
| title_short | Sound and automated synthesis of digital stabilizing controllers for continuous plants |
| title_sort | sound and automated synthesis of digital stabilizing controllers for continuous plants |
| work_keys_str_mv | AT abatea soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants AT bessai soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants AT cattaruzzad soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants AT cordeirol soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants AT davidc soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants AT kesselip soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants AT kroeningd soundandautomatedsynthesisofdigitalstabilizingcontrollersforcontinuousplants |