The increased adoption and deployment of cyber-physical systems in critical infrastructure in recent years have led to challenging questions about safety and reliability. These systems usually operate in uncertain environments and are required to satisfy a broad spectrum of specifications. Thus, automated tools are necessary to alleviate the need for manual design and proof of their correct behaviors. This thesis studies mathematical and computational frameworks to design correct and optimal control strategies for discrete-time and continuous-time systems with temporal and spatial specifications. Signal Temporal Logic (STL) is employed as a rich and expressive language to impose temporal constraints and deadlines on system performance.
The first part of the thesis introduces a novel quantitative semantics for STL that improves the evaluation of temporal logic specifications. Furthermore, an extension of STL, called Weighted Signal Temporal Logic (wSTL), is defined in order to formalize satisfaction priorities of multiple specifications and time preferences in a high-level specification. Learning-based frameworks are proposed to infer quantitative semantics, and satisfaction priorities and preferences from data.
The second part develops optimization frameworks to determine control strategies enforcing the satisfaction of wSTL specifications by different classes of systems. Mixed-integer programming and gradient-based optimization techniques are studied to solve the control synthesis problem. Further evaluation and optimization algorithms are presented based on Control Barrier Functions to guarantee continuous-time satisfaction of safety-critical specifications in a system.
The third part of this thesis focuses on utilizing STL to express spatio-temporal specifications that are widely used in networks of locally interacting dynamical systems. Machine learning techniques are used to derive spatio-temporal quantitative semantics, which is employed in automated frameworks for evaluation and synthesis of complex spatial and temporal properties. Case studies illustrating the synthesis of spatio-temporal patterns in biological cell networks are presented.
| Identifer | oai:union.ndltd.org:bu.edu/oai:open.bu.edu:2144/41871 |
| Date | 11 January 2021 |
| Creators | Mehdipour, Noushin |
| Contributors | Belta, Calin |
| Source Sets | Boston University |
| Language | en_US |
| Detected Language | English |
| Type | Thesis/Dissertation |
Page generated in 0.002 seconds