The future where non-autonomous systems like human-driven cars are replaced by autonomous, driverless cars is now within reach. This reduction in human effort comes at a cost: in existing systems, human operators implicitly define high-level system objectives through their actions; autonomous systems lack this guidance. Popular design techniques for autonomy such as those based on deep reinforcement learning obtain such guidance from user-specified, state-based reward functions or user-provided demonstrations. Unfortunately, such techniques generally do not provide guarantees on the safe behavior of the trained controllers. This project argues for a different approach where mathematically unambiguous, system-level behavioral specifications expressed in temporal logic are used to guide deep reinforcement learning algorithms to train neural network-based controllers. It allows reasoning about the safety of learning-based control through scalable methods for formal verification of the trained controllers against the given specifications.

To address lack of explainability of neural controllers, this project devises new techniques to distill the neural-network-controlled autonomous system into human-interpretable symbolic automata. The project blends methods from statistical learning, control theory, optimization, and formal methods to give deterministic or probabilistic guarantees on the safe behavior of autonomous systems. It integrates education and research through new graduate courses on verifiable reinforcement learning. The investigator will broadly disseminate the scientific outcomes of the project through technology transfer to industrial partners and through publications at top research conferences and journals. The expected societal impact is improved safety and explainable control for future autonomous cyber-physical systems in various application domains.