Title | Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics |
Publication Type | Conference Paper |
Year of Publication | 2018 |
Authors | Fan C, Mathur U, Mitra S, Viswanathan M |
Conference Name | Computer Aided Verification - 30th International Conference, (CAV) |
Date Published | jul |
Publisher | Springer, Cham |
Conference Location | Oxford, UK |
Abstract | 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 overapproximated 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. |
URL | http://link.springer.com/10.1007/978-3-319-96145-3{\_}19 |
DOI | 10.1007/978-3-319-96145-3_19 |
Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics
Submitted by chuchu@mit.edu on