Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Alessandro  Abate; Lury Bessa; Dario Cattaruzza; Lucas  Cordeiro; Cristina David; Pascal Kesseli; Daniel  Kroening

doi:10.1145/3049797.3049802

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Alessandro Abate, Lury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

15 Citations (Scopus)

71 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems
Subtitle of host publication	Computation and Control
Publisher	Association for Computing Machinery (ACM)
Pages	197–206
Number of pages	10
DOIs	https://doi.org/10.1145/3049797.3049802
Publication status	Published - 18 Apr 2017
Event	ACM International Conference on Hybrid Systems: Computation and Control - Pittsburgh, United States Duration: 18 Apr 2017 → 20 Apr 2017 Conference number: 20 http://hscc2017.ece.illinois.edu/

Conference

Conference	ACM International Conference on Hybrid Systems
Abbreviated title	HSCC 2017
Country/Territory	United States
City	Pittsburgh
Period	18/04/17 → 20/04/17
Internet address	http://hscc2017.ece.illinois.edu/

Research Groups and Themes

Programming Languages

Access to Document

10.1145/3049797.3049802

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via ACM at https://dl.acm.org/doi/10.1145/3049797.3049802. Please refer to any applicable terms of use of the publisher.
Final published version, 1.12 MBLicence: CC BY

Handle.net

Persistent link

Embargoed Document

Full-text PDF (accepted author manuscript)
Accepted author manuscript, 445 KB

Dr Cristina David
- cristina.davidbristol.acuk
- School of Computer Science - Senior Lecturer
Person: Academic

Cite this

Abate, A., Bessa, L., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., & Kroening, D. (2017). Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. In HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (pp. 197–206). Association for Computing Machinery (ACM). https://doi.org/10.1145/3049797.3049802

@inproceedings{f6bb8a354b524232bea5f0a412670785,

title = "Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants",

abstract = "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.",

author = "Alessandro Abate and Lury Bessa and Dario Cattaruzza and Lucas Cordeiro and Cristina David and Pascal Kesseli and Daniel Kroening",

year = "2017",

month = apr,

day = "18",

doi = "10.1145/3049797.3049802",

language = "English",

pages = "197–206",

booktitle = "HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "ACM International Conference on Hybrid Systems : Computation and Control, HSCC 2017 ; Conference date: 18-04-2017 Through 20-04-2017",

url = "http://hscc2017.ece.illinois.edu/",

}

Abate, A, Bessa, L, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P & Kroening, D 2017, Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. in HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. Association for Computing Machinery (ACM), pp. 197–206, ACM International Conference on Hybrid Systems, Pittsburgh, Pennsylvania, United States, 18/04/17. https://doi.org/10.1145/3049797.3049802

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. / Abate, Alessandro ; Bessa, Lury; Cattaruzza, Dario et al.
HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. Association for Computing Machinery (ACM), 2017. p. 197–206.

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

TY - GEN

T1 - Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

AU - Abate, Alessandro

AU - Bessa, Lury

AU - Cattaruzza, Dario

AU - Cordeiro, Lucas

AU - David, Cristina

AU - Kesseli, Pascal

AU - Kroening, Daniel

N1 - Conference code: 20

PY - 2017/4/18

Y1 - 2017/4/18

N2 - 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.

AB - 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.

U2 - 10.1145/3049797.3049802

DO - 10.1145/3049797.3049802

M3 - Conference Contribution (Conference Proceeding)

SP - 197

EP - 206

BT - HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems

PB - Association for Computing Machinery (ACM)

T2 - ACM International Conference on Hybrid Systems

Y2 - 18 April 2017 through 20 April 2017

ER -

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Abstract

Conference

Research Groups and Themes

Access to Document

Handle.net

Embargoed Document

Fingerprint

Profiles

Dr Cristina David

Cite this