TY - GEN
T1 - Verified hybrid LQ control for autonomous spacecraft rendezvous
AU - Chan, Nicole
AU - Mitra, Sayan
N1 - Funding Information:
We thank Richard S. Erwin for providing the MPC controller tested here, and Bolun Qi for support with the verification experiments. This work was supported by NSF grants: CNS 1629949, CNS 1054247, and CCF 1422798.
Publisher Copyright:
© 2017 IEEE.
PY - 2018/1/18
Y1 - 2018/1/18
N2 - Rendezvous is a fundamental maneuver in autonomous space operations in which an active chaser spacecraft is required to navigate safely to the proximity of a second passive target spacecraft. Ensuring safety of such control maneuvers is challenging and design errors can be expensive. We present the first verified control solution to a benchmark formulation of spacecraft autonomous rendezvous in the form of a hybrid LQR controller verified using a data-driven algorithm. Our hybrid LQR scheme is motivated by enforcing safety constraints rather than optimizing performance, and the control law is formulated by periodically solving optimization problems that depend on the current state. The resulting hybrid system presents a challenge for existing automated formal verification tools due to its lack of a closed-form model description. We overcome this challenge by using a data-driven approach (implemented in the new verification tool DryVR). DryVR relies on simulation traces to compute reachable states of the system over bounded time horizon and initial conditions to rigorously verify that the system does not violate any safety requirements.
AB - Rendezvous is a fundamental maneuver in autonomous space operations in which an active chaser spacecraft is required to navigate safely to the proximity of a second passive target spacecraft. Ensuring safety of such control maneuvers is challenging and design errors can be expensive. We present the first verified control solution to a benchmark formulation of spacecraft autonomous rendezvous in the form of a hybrid LQR controller verified using a data-driven algorithm. Our hybrid LQR scheme is motivated by enforcing safety constraints rather than optimizing performance, and the control law is formulated by periodically solving optimization problems that depend on the current state. The resulting hybrid system presents a challenge for existing automated formal verification tools due to its lack of a closed-form model description. We overcome this challenge by using a data-driven approach (implemented in the new verification tool DryVR). DryVR relies on simulation traces to compute reachable states of the system over bounded time horizon and initial conditions to rigorously verify that the system does not violate any safety requirements.
UR - http://www.scopus.com/inward/record.url?scp=85046136160&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85046136160&partnerID=8YFLogxK
U2 - 10.1109/CDC.2017.8263854
DO - 10.1109/CDC.2017.8263854
M3 - Conference contribution
AN - SCOPUS:85046136160
T3 - 2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017
SP - 1427
EP - 1432
BT - 2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 56th IEEE Annual Conference on Decision and Control, CDC 2017
Y2 - 12 December 2017 through 15 December 2017
ER -