Adaptive optimization framework for verification and control of cyber-physical systems

Abstract

The main focus of this thesis is an optimization-based framework for control and verification of cyber-physical systems that synthesizes actions steering a given system towards a specified state. The primary motivation for the research presented in this thesis is a fascination with birds, which save energy on long-distance flights via forming a V-shape. We ask the following question: Are V-formations a result of solving an optimization problem and can this concept be utilized in cyber-physical systems, particularly in drone swarms, to increase their safety and resilience? In this thesis, we combine the state-of-the-art in statistical model checking and optimizationbased control for nonlinear systems. First, we propose a control-based evaluation of the probability of rare events that can lead to fatal accidents involving cyber-physical systems. Second, we synthesize controllers for a flock of birds modeled as a stochastic multi-agent system equipped with a highly nonlinear cost function. Further, we show that the proposed control approach is stable with respect to rare events, i.e., it leads to a successful recovery of the optimal formation from several types of malicious attacks. Finally, we investigate the ways to efficiently distribute control among the agents. We demonstrate that our framework can be applied to any system modeled as a controllable Markov decision process with a cost (reward) function. A key feature of the procedure we propose is its automatic adaptation to the convergence performance of optimization towards a given global objective. Combining model-predictive control and ideas from sequential Monte-Carlo methods, we introduce a performance-based adaptive horizon and implicitly build a Lyapunov function that guarantees convergence. We use statistical model-checking to verify the algorithm and assess its reliability.