PhD Thesis Proposal - Navid Hashemi

Title: Verification and Synthesis of Controllers for Temporal Logic Objectives Using Neuro-Symbolic Methods
 
Committee Members: Jyotirmoy Deshmukh (Chair), Guarav Sukhatme, Chao Wang, Pierlggi Nuzzo, Lars Lindemann, Georgios Fainekos (External Member)     
 
Date & Time: Thursday, April 25th, 10:30am - 12:00pm
 
Abstract: As the field of autonomy is embracing the use of neural networks for perception and control, Signal Temporal Logic (STL) has emerged as a popular formalism for specifying the task objectives and safety properties of such autonomous cyber-physical systems (ACPS). There are two important open problems in this research area: (1) how can we effectively train neural controllers in such ACPS applications, when the state dimensionality is high and when the task objectives are specified over long time horizons, and (2) how can we verify if the closed-loop system with a given neural controller satisfies given STL objectives. We review completed work in which we show how discrete-time STL (DT-STL) specifications lend themselves to a smooth neuro-symbolic encoding that enables the use of gradient-based methods for control design. We also show how a type of neuro-symbolic encoding of DT-STL specifications can be combined with neural network verification tools to provide deterministic guarantees. We also review how neural network encoding of the environment dynamics can help us combine statistical verification techniques with formal techniques for reachability analysis. We will then propose several directions that we will pursue in the future: (1) We will investigate if our neuro-symbolic encoding approach can extend to other temporal logics, especially those used for specifying properties of perception algorithms (such as Spatio-Temporal Perception Logic or STPL). Our idea is to use a neuro-symbolic encoding of STPL to improve the quality of outputs produced by perception algorithms. (2) We will investigate how control policies generated by our existing algorithms can be made robust to distribution shifts through online and offline techniques. (3) Finally, we will propose scaling our synthesis approaches to higher-dimensional observation spaces and longer horzon tasks. We conclude with the timeline to finish proposed work and write the dissertation.

Location: Ronald Tutor Hall of Engineering (RTH) - 306

Audiences: Everyone Is Invited

Contact: Felante' Charlemagne