Towards Verified Control and Machine Learning of Cyber Physical Systems: A Formal Methods Perspective  

ABSTRACT

Recent years have seen a growing interest in control and learning of cyber physical systems (CPS), which involve multiple physical components monitored and controlled by computational units exchanging information. The increasing demands for safety, security and efficiency put stringent constraints on verification and design of CPS. The fundamental question is how to produce verifiable and provably correct results, which necessitates the use of formal methods. This talk will present some results towards formally verified model based control and model free learning.

The first part of the talk focuses on higher level control logic of CPS under the framework of discrete event systems (DES). Specifically, two important topics in DES will be discussed: cyber security and supervisory control. The first topic concerns an information flow based security property called opacity and insertion/edit functions are developed to enforce opacity against malicious inference of intruders. The second topic considers synthesizing energy aware supervisors that enforce required properties by restricting the system behaviors under both qualitative and quantitative constraints. Results from algorithmic game theory are leveraged for synthesis purposes to solve the two problems under appropriate game theoretic settings. The second part introduces verified machine learning, which incorporates formal methods and optimal control into machine learning. A formal methods guided safe reinforcement learning approach is proposed for dynamic control systems exploring unknown environments. Temporal logic properties formally define the tasks with a priori knowledge and guide the learning agent to fulfill the tasks. Unsafe behaviors are explicitly defined from the formal language, then control barrier functions are deployed to guarantee safety during learning. Optimal strategies are synthesized on the fly, which are correct by construction and scale well. Potential applications include robot path planning, autonomous vehicles and driver assistant technologies. Ongoing works on trusted and verified artificial intelligence will be briefly mentioned in the end.