Machine learning and data-driven techniques for verification and synthesis of cyber-physical systems

Salamati, Ali (2023): Machine learning and data-driven techniques for verification and synthesis of cyber-physical systems. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

Safety and performance are the most important requirements for designing and manufacturing complex life-critical systems. Consider a self-driving car which is not equipped with certain safety functionalities. It can cause fatal accidents, severe injuries, or serious damages to the environment. Hence, rigorous analysis required to ensure the correctness of functionalities in many safety-critical applications. Model-based approaches for satisfying such requirements have been studied extensively in the literature. Unfortunately, a precise model of the system is not always available in many practical scenarios. Hence, in this thesis we focus on data-driven methods and machine learning techniques to tackle this challenge. First, we assume that only an incomplete parameterized model of the system is available. The main goal is to study formal verification of linear time-invariant systems with respect to a fragment of temporal logic specifications when only a partial knowledge of the model is available, i.e., a parameterized model of the system is known but the exact values of the parameters are unknown. We provide a probabilistic measure for the satisfaction of the specification by trajectories of the system under the influence of uncertainty. We assume that these specifications are expressed as signal temporal logic formulae and provide an approach that relies on gathering input-output data from the system. We employ Bayesian inference on the collected data to associate a notion of confidence with the satisfaction of the specification. Second, we assume that we do not have any knowledge about the model of the system and just have access to input-output data from the system. We study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, notion of barrier certificates have been successfully applied for ensuring the satisfaction of safety specifications. Here, we formulate the computation of barrier certificates as a robust convex program (RCP). Solving the acquired RCP is difficult in general because the model of the system that appears in one of the constraints of the RCP is unknown. We propose a data-driven approach that replaces the uncountable number of constraints in the RCP with a finite number of constraints by taking finitely many random samples from the trajectories of the system. We thus replace the original RCP with a scenario convex program (SCP) and show how to relate their optimizers. We guarantee that the solution of the SCP is a solution of the RCP with a priori guaranteed confidence when the number of samples is larger than a specific value. This provides a lower bound on the safety probability of the original unknown system together with a controller in the case of synthesis. Lastly, to address the high demand for data in our data-driven barrier-based approach, we propose three remedies. First, the wait-and-judge approach that checks a condition over the optimal value of the SCP using a fixed number of samples, ensuring a lower bound probability and the desired confidence for satisfying safety specifications. Second, the repetition-based scenario framework that iteratively solves the SCP with samples, checking feasibility and achieving the desired violation error. A safety condition is verified, enabling the computation of a lower bound for safety satisfaction. Third, the wait, judge, and repeat framework that solves the SCP iteratively until a feasibility condition, based on computed support constraints, is met. If the safety condition is satisfied, the system is considered safe with a lower bound probability determined using the optimizer of the successful iteration.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Machine Learning, Stochastic System, Data-driven Techniques, Safety of AI
• Themengebiete: 000 Allgemeines, Informatik, Informationswissenschaft ; 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 4. Oktober 2023
• 1. Bericht­erstatter:in: Zamani, Majid