A Verification Framework for Certifying Learning-Based Safety-Critical Aviation Systems

We present a safety verification framework for design-time and run-time assurance of learning-based components in aviation systems. Our proposed framework integrates two novel methodologies. From the design-time assurance perspective, we propose offline mixed-fidelity verification tools that incorporate knowledge from different levels of granularity in simulated environments. From the run-time assurance perspective, we propose reachability- and statistics-based online monitoring and safety guards for a learning-based decision-making model to complement the offline verification methods. This framework is designed to be loosely coupled among modules, allowing the individual modules to be developed using independent methodologies and techniques, under varying circumstances and with different tool access. The proposed framework offers feasible solutions for meeting system safety requirements at different stages throughout the system development and deployment cycle, enabling the continuous learning and assessment of the system product.

Control of Magnetic Microrobot Teams for Temporal Micromanipulation Tasks

In this paper, we present a control framework that allows magnetic microrobot teams to accomplish complex micromanipulation tasks captured by global Linear Temporal Logic (LTL) formulas. To address this problem, we propose an optimal control synthesis method that constructs discrete plans for the robots that satisfy both the assigned tasks as well as proximity constraints between the robots due to the physics of the problem. Our proposed algorithm relies on an existing optimal control synthesis approach combined with a novel sampling-based technique to reduce the state-space of the product automaton that is associated with the LTL specifications. The synthesized discrete plans are executed by the microrobots independently using local magnetic fields. Simulation studies show that the proposed algorithm can address large-scale planning problems that cannot be solved using existing optimal control synthesis approaches. Moreover, we present experimental results that also illustrate the potential of our method in practice. To the best of our knowledge, this is the first control framework that allows independent control of teams of magnetic microrobots for temporal micromanipulation tasks.