Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lucas Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen

doi:10.1007/978-3-319-63387-9_23

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

Original language	English
Title of host publication	Computer Aided Verification
Editors	Rupak Majumdar, Viktor Kunčak
Place of Publication	Cham
Publisher	Springer International Publishing
Pages	462-482
Number of pages	21
ISBN (Electronic)	978-3-319-63387-9
ISBN (Print)	978-3-319-63386-2
DOIs	https://doi.org/10.1007/978-3-319-63387-9_23
Publication status	Published - 13 Jul 2017
Event	29th International Conference on Computer Aided Verification - Heidelberg, Germany Duration: 24 Jul 2017 → 28 Jul 2017 http://cavconference.org/2017/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Volume	10426
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	29th International Conference on Computer Aided Verification
Abbreviated title	CAV 2017
Country/Territory	Germany
City	Heidelberg
Period	24/07/17 → 28/07/17
Internet address	http://cavconference.org/2017/

Access to Document

10.1007/978-3-319-63387-9_23Licence: All Rights Reserved

https://link.springer.com/chapter/10.1007/978-3-319-63387-9_23Licence: All Rights Reserved

Elizabeth Polgreen
- School of Informatics - Lecturer in Programming Languages for Trustworthy Systems
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active

Cite this

Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D., & Polgreen, E. (2017). Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. In R. Majumdar, & V. Kunčak (Eds.), Computer Aided Verification (pp. 462-482). ( Lecture Notes in Computer Science ; Vol. 10426). Springer International Publishing. https://doi.org/10.1007/978-3-319-63387-9_23

Abate, Alessandro ; Bessa, Iury ; Cattaruzza, Dario ; Cordeiro, Lucas ; David, Cristina ; Kesseli, Pascal ; Kroening, Daniel ; Polgreen, Elizabeth. / Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. Computer Aided Verification. editor / Rupak Majumdar ; Viktor Kunčak. Cham : Springer International Publishing, 2017. pp. 462-482 ( Lecture Notes in Computer Science ).

@inproceedings{11cd079cb7ee4224a2a3a258c01ba39e,

title = "Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants",

abstract = "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 digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.",

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

year = "2017",

month = jul,

day = "13",

doi = "10.1007/978-3-319-63387-9_23",

language = "English",

isbn = "978-3-319-63386-2",

series = " Lecture Notes in Computer Science ",

publisher = "Springer International Publishing",

pages = "462--482",

editor = "Rupak Majumdar and Viktor Kun{\v c}ak",

booktitle = "Computer Aided Verification",

note = "29th International Conference on Computer Aided Verification, CAV 2017 ; Conference date: 24-07-2017 Through 28-07-2017",

url = "http://cavconference.org/2017/",

}

Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P, Kroening, D & Polgreen, E 2017, Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. in R Majumdar & V Kunčak (eds), Computer Aided Verification. Lecture Notes in Computer Science , vol. 10426, Springer International Publishing, Cham, pp. 462-482, 29th International Conference on Computer Aided Verification, Heidelberg, Germany, 24/07/17. https://doi.org/10.1007/978-3-319-63387-9_23

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. / Abate, Alessandro; Bessa, Iury; Cattaruzza, Dario; Cordeiro, Lucas; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth.

Computer Aided Verification. ed. / Rupak Majumdar; Viktor Kunčak. Cham : Springer International Publishing, 2017. p. 462-482 ( Lecture Notes in Computer Science ; Vol. 10426).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

AU - Abate, Alessandro

AU - Bessa, Iury

AU - Cattaruzza, Dario

AU - Cordeiro, Lucas

AU - David, Cristina

AU - Kesseli, Pascal

AU - Kroening, Daniel

AU - Polgreen, Elizabeth

PY - 2017/7/13

Y1 - 2017/7/13

N2 - 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 digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

AB - 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 digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.

U2 - 10.1007/978-3-319-63387-9_23

DO - 10.1007/978-3-319-63387-9_23

M3 - Conference contribution

SN - 978-3-319-63386-2

T3 - Lecture Notes in Computer Science

SP - 462

EP - 482

BT - Computer Aided Verification

A2 - Majumdar, Rupak

A2 - Kunčak, Viktor

PB - Springer International Publishing

CY - Cham

T2 - 29th International Conference on Computer Aided Verification

Y2 - 24 July 2017 through 28 July 2017

ER -

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Abstract

Publication series

Conference

Access to Document

Fingerprint

Profiles

Elizabeth Polgreen

Cite this