Title: Adaptive optimization framework for verification and control of cyber-physical systems
Language: English
Authors: Lukina, Anna 
Qualification level: Doctoral
Advisor: Grosu, Radu
Issue Date: 2018
Number of Pages: 110
Qualification level: Doctoral
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.
Keywords: cyber physical systems; control synthesis; statistical model checking; Markov decision processes; model predictive control; flocking; adaptive optimization; drones; V formation; sequential Monte-Carlo methods
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-127016
http://hdl.handle.net/20.500.12708/8606
Library ID: AC15406841
Organisation: E191 - Institut für Computer Engineering 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

24
checked on Jun 15, 2021

Download(s)

40
checked on Jun 15, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.