My research lies at the intersection of formal methods for reasoning about software and systems, foundations of cyber-physical systems (CPS), control theory, and mathematical logic. I am increasingly interested in reasoning about real-world CPS applications that use AI components trained with machine learning algorithms. Here are some of the topics on which I am actively working:

Learning from Time-series Data

Numerous machine learning techniques have been proposed for supervised learning (classification), unsupervised learning (clustering), causality analysis, and anomaly detection for time-series data. These techniques are very powerful, giving highly accurate results for large data-sets. However, the results of learning may not always be interpretable (e.g. what do all data belonging to a particular cluster have in common? or why does the decision boundary separate two given examples). We explore the use of formal logics for supervised classification, unsupervised learning, mining information from positive examples, and mining requirements from cyber-physical system models. Specifically, we focus on learning Signal Temporal Logic formulas from data, and develop the new formalism of Shape Expressions for these tasks.

Supported by NSF Award: 1837131. FMitF: A Novel Framework for Learning Formal Abstractions and Causal Relations from Temporal Behaviors.

Runtime Monitoring

Cyberphysical systems such as autonomous aerial and ground vehicles, industrial control systems, medical devices, power grids and many others are highly complex. In very limited scenarios, formal verification techniques can digest the scale and complexity of such techniques, and even then verification guarantees correctness of a software model of the system, and not the actual deployed system. Runtime monitoring is a valuable tool to check dynamic correctness of such systems, and coupled with runtime safety enforcement can be a powerful method to assure system correctness. In particular, we are interested in monitoring temporal and logical requirements of such systems. There are several flavors of monitoring: offline or batch monitoring records temporal data about the system behaviors and runs (asynchronously) runs monitoring algorithms on the recorded data. Online monitoring checks past-time or future-time temporal logic formulas synchronously with the system. Predictive monitoring or hidden state monitors check satisfaction/violation of temporal logic formulas on hidden system states by only looking at the observable behaviors. Finally, clairvoyant monitoring is about monitoring future-time temporal logic formulas on predicted system behaviors.

Supported by NSF Award CCF/SHF-1910088: Premonition: A Methodology for Predictive Monitoring with Probabilistic Guarantees

Safe Intelligent Control

How do we design neural network controllers to respect high-level requirements? How do we verify safety of neural network controllers? In this research, we tackle such problems.

TBD Supported by a grant from Toyota R&D