Data-driven machine learning (ML) components have been deployed in multiple cyber-physical systems, from sensing and perception to planning and control. However, the reliability and safety of such ML-based applications remain the most challenging and significant concern for the industry, users, and regulators. Rigorous effort has been made to develop formal methods for ML-based application certification. Most research focuses on qualitative verification of the safety and robustness of neural networks and neural network control systems. There is a lack of methods that can quantitatively verify the temporal properties of ML-based applications, which has been a problem of keen interest for industrial companies in the automotive industry, as quantitative verification results, e.g., probability of collision, provide richer information for better decision-making and planning of autonomous systems under sensing, perception and actuating uncertainties. This project proposes to continue collaborations with industrial partners to develop a new quantitative verification approach for temporal properties of learning-enabled cyber-physical systems (Le-CPS). The project's novelties are the development of new ProbStar Temporal Logic (PSTL) for specifying complex temporal behaviors of Le-CPS and new qualitative and quantitative verification algorithms for verifying Le-CPS temporal properties. The project's impact is supporting transitioning advanced verification technologies into practice v