Show simple item record

dc.contributor.authorAbate, Alessandro
dc.contributor.authorBessa, Iury
dc.contributor.authorCordeiro, Lucas
dc.contributor.authorDavid, Cristina
dc.contributor.authorKesseli, Pascal
dc.contributor.authorKroening, Daniel
dc.contributor.authorPolgreen, Elizabeth
dc.date.accessioned2020-12-05T16:13:21Z
dc.date.available2020-12-05T16:13:21Z
dc.date.issued2019-12-06
dc.date.submitted2019-02-01
dc.identifier.issn0001-5903
dc.identifier.others00236-019-00359-1
dc.identifier.other359
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/314802
dc.description.abstractAbstract: We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as time-invariant models. Models are linear differential equations with inputs, evolving over a continuous state space. The synthesis precisely accounts for the effects of finite-precision arithmetic introduced by the controller. The approach uses counterexample-guided inductive synthesis: an inductive generalization phase produces a controller that is known to stabilize the model but that may not be safe for all initial conditions of the model. Safety is then verified via bounded model checking: if the verification step fails, a counterexample is provided to the inductive generalization, and the process further iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for physical plant models from the digital control literature.
dc.languageen
dc.publisherSpringer Berlin Heidelberg
dc.rightsAttribution 4.0 International (CC BY 4.0)en
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en
dc.subjectOriginal Article
dc.titleAutomated formal synthesis of provably safe digital controllers for continuous plants
dc.typeArticle
dc.date.updated2020-12-05T16:13:20Z
prism.endingPage244
prism.issueIdentifier1-2
prism.publicationNameActa Informatica
prism.startingPage223
prism.volume57
dc.identifier.doi10.17863/CAM.61909
dcterms.dateAccepted2019-11-25
rioxxterms.versionofrecord10.1007/s00236-019-00359-1
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/
dc.contributor.orcidAbate, Alessandro [0000-0002-5627-9093]
dc.contributor.orcidBessa, Iury [0000-0002-6603-3476]
dc.contributor.orcidCordeiro, Lucas [0000-0002-6235-4272]
dc.contributor.orcidDavid, Cristina [0000-0002-9106-934X]
dc.contributor.orcidKesseli, Pascal [0000-0003-0300-5598]
dc.contributor.orcidKroening, Daniel [0000-0002-6681-5283]
dc.contributor.orcidPolgreen, Elizabeth [0000-0001-9032-7661]
dc.identifier.eissn1432-0525
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/J012564/1)
pubs.funder-project-idEuropean Research Council (280053)
pubs.funder-project-idH2020 Future and Emerging Technologies (280053)


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International (CC BY 4.0)
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)