Research

My research focus is on incorporating temporal logic formalism with machine learning framework in order to capture and alter system specifications from data.

Formal methods are originally developed for specification and verification of software systems. Formal methods aim to provide mathematical analysis and proofs to system’s performance. In particular, temporal logic is a formal method which is initially used for verification.

Recent works in control field benefit from temporal logic to specify system’s behavior, constraints, and task objectives for systems. Specifications written in temporal logic formalism can be used for application areas like control synthesis, motion planning. However, for many systems, specifying system’s behavior can be challenging even in plain English. We can get help from system trajectories to understand the underlying rules. Inferring information from data calls machine learning and data analysis into the scene.