Model predictive control provides an optimal solution for driving dynamical systems that also guarantees constraints on the system's behavior are obeyed. However, as the system model and/or its constraints becomes more complex, MPC becomes a computationally expensive and it becomes unclear what solution will actually be found at runtime.
I'm exploring ways to relax the optimization problem, compute closed-form solutions, and apply formal verification schemes to the problem to check that all possible behaviors of the system do obey the constraints.
The CyPhyHouse team is developing a high-level programming language framework (Koord) for streamlining development of distributed robotic applications. This makes the process accessible to a wider demographic (e.g. appropriate for education/outreach), enables researchers to efficiently test algorithms on virtually any robot platform, and lays a foundation for us to incorporate verification at compile time.
I am assembling a fleet of small-scale autonomous ground vehicles (based off the F1/10 platform) called ARCaDe, on which we will deploy and test Koord.
During my internship at the Air Force Research Lab (2016), I studied a benchmark hybrid model of a fundamental maneuver for autonomous spacecraft navigation called Rendezvous. I modeled the system and its constraints to run through well-established verification tools: C2E2 and SpaceEx. Furthermore, I implemented an alternate reachability algorithm for this spacecraft problem in Matlab (dubbed SDVTool). Overview of this work and related past work can be found here. I presented this work at the ARCH workshop of the 2017 CPS Week conference.
This concept has been around since ALVINN in the 90s and continues to be a popular, promising approach. We are exploring this option for controlling the ARCaDe cars. We have modeled CSL and one of the cars in the Unity gaming engine, and are training and testing in the game world. We'd like to study the effects and nature of adversarial examples using the controlled environment in Unity.
Verified hybrid LQ control for autonomous spacecraft rendezvous. Nicole Chan and Sayan Mitra. In the 56th IEEE Conference on Decision and Control (CDC 2017).
Verifying safety of an autonomous spacecraft rendezvous mission. Nicole Chan and Sayan Mitra. In the 4th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2017).
CODEV: Automated Model Predictive Control Design and Formal Verification (Tool Paper). Nicole Chan and Sayan Mitra. In the 21st International Conference on Hybrid Systems: Computation and Control (HSCC 2018).
ROS workspace for the original F1/10 car buildand the modified second build.
Full software stack for the CyPhyHouse project (implemented on the aforementioned cars as well as quadcopters).