Verified hybrid LQ control for autonomous spacecraft rendezvous

Nicole Chan, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1427-1432
Number of pages6
ISBN (Electronic)9781509028733
DOIs
StatePublished - Jan 18 2018
Event56th IEEE Annual Conference on Decision and Control, CDC 2017 - Melbourne, Australia
Duration: Dec 12 2017Dec 15 2017

Publication series

Name2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017
Volume2018-January

Other

Other56th IEEE Annual Conference on Decision and Control, CDC 2017
Country/TerritoryAustralia
CityMelbourne
Period12/12/1712/15/17

ASJC Scopus subject areas

  • Decision Sciences (miscellaneous)
  • Industrial and Manufacturing Engineering
  • Control and Optimization

Fingerprint

Dive into the research topics of 'Verified hybrid LQ control for autonomous spacecraft rendezvous'. Together they form a unique fingerprint.

Cite this