Speaker: Mingshuai Chen
Abstract: This talk addresses the problem of inferring a hybrid automaton from a set of input-output traces of a hybrid system exhibiting discrete mode switching between continuously evolving dynamics. Existing approaches mainly adopt a derivative-based method where (i) the occurrence of mode switching is determined by a drastic variation in derivatives and (ii) the clustering of trace segments relies on signal similarity – both subject to user-supplied thresholds. In this talk, I present a derivative-agnostic approach, named Dainarx, to infer nonlinear hybrid systems where the dynamics are captured by nonlinear autoregressive exogenous (NARX) models. Dainarx employs NARX models as a unified, threshold-free representation through the detection of mode switching and trace-segment clustering. We show that Dainarx suffices to learn models that closely approximate a general class of hybrid systems featuring high-order nonlinear dynamics with exogenous inputs, nonlinear guard conditions, and linear resets. Experimental results on a collection of benchmarks indicate that our approach can effectively and efficiently infer nontrivial hybrid automata with high-order dynamics yielding significantly more accurate approximations than state-of-the-art techniques.
Bio: Mingshuai Chen is an Assistant Professor leading the Formal Verification Group at Zhejiang University (ZJU), Hangzhou, China. Prior to joining ZJU, he worked as a Postdoctoral Researcher at RWTH Aachen University in Germany. In 2019, he received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences. Mingshuai Chen’s research interests include formal verification, synthesis, programming theory, and cyber-physical systems, broadly construed in theoretical aspects of computer science. He has co-authored peer-reviewed papers at flagship journals/conferences including Inf. Compt., IEEE Trans. Automat. Contr., OOPSLA, CAV, FM, ASPLOS, IJCAR, TACAS etc. He was the awardee of the Distinguished Paper Award at ATVA 2018, Best Paper Award at FMAC 2019, and the CAS-President Special Award in 2019. Mingshuai Chen is the recipient of the NSFC Excellent Young Scientists Fund Program (Overseas), which is known as one of the most prestigious grants for young researchers across China. His research results have been partially applied in the verification of control programs of the Chinese lunar lander Chang’e-3 and the Chinese high-speed railway system.