@inproceedings{ec824a4c569d4f7497c510aec33926f7,
title = "Verified hybrid LQ control for autonomous spacecraft rendezvous",
abstract = "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.",
author = "Nicole Chan and Sayan Mitra",
note = "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.; 56th IEEE Annual Conference on Decision and Control, CDC 2017 ; Conference date: 12-12-2017 Through 15-12-2017",
year = "2017",
month = jun,
day = "28",
doi = "10.1109/CDC.2017.8263854",
language = "English (US)",
series = "2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1427--1432",
booktitle = "2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017",
address = "United States",
}