TY - GEN
T1 - Controller Synthesis Made Real
T2 - 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
AU - Fan, Chuchu
AU - Mathur, Umang
AU - Mitra, Sayan
AU - Viswanathan, Mahesh
N1 - Funding Information:
This work is supported by the grant CCF 1422798 from the National Science Foundation.
Publisher Copyright:
© The Author(s) 2018.
PY - 2018
Y1 - 2018
N2 - We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Our solution uses a combination of an open-loop controller and a tracking controller, thereby reducing the problem to smaller tractable problems. We show that, once a tracking controller is fixed, the reachable states from an initial neighborhood, subject to any disturbance, can be over-approximated by a sequence of ellipsoids, with sizes that are independent of the open-loop controller. Hence, the open-loop controller can be synthesized independently to meet the reach-avoid specification for an initial neighborhood. Exploiting several techniques for tightening the over-approximations, we reduce the open-loop controller synthesis problem to satisfiability over quantifier-free linear real arithmetic. The overall synthesis algorithm, computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We present RealSyn, a tool implementing this synthesis algorithm, and we show that it scales to several high-dimensional systems with complex reach-avoid specifications.
AB - We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Our solution uses a combination of an open-loop controller and a tracking controller, thereby reducing the problem to smaller tractable problems. We show that, once a tracking controller is fixed, the reachable states from an initial neighborhood, subject to any disturbance, can be over-approximated by a sequence of ellipsoids, with sizes that are independent of the open-loop controller. Hence, the open-loop controller can be synthesized independently to meet the reach-avoid specification for an initial neighborhood. Exploiting several techniques for tightening the over-approximations, we reduce the open-loop controller synthesis problem to satisfiability over quantifier-free linear real arithmetic. The overall synthesis algorithm, computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We present RealSyn, a tool implementing this synthesis algorithm, and we show that it scales to several high-dimensional systems with complex reach-avoid specifications.
UR - http://www.scopus.com/inward/record.url?scp=85051143714&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85051143714&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-96145-3_19
DO - 10.1007/978-3-319-96145-3_19
M3 - Conference contribution
AN - SCOPUS:85051143714
SN - 9783319961446
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 347
EP - 366
BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
A2 - Weissenbacher, Georg
A2 - Chockler, Hana
PB - Springer
Y2 - 14 July 2018 through 17 July 2018
ER -