Formal methods for resilient control
MetadataShow full item record
Many systems operate in uncertain, possibly adversarial environments, and their successful operation is contingent upon satisfying specific requirements, optimal performance, and ability to recover from unexpected situations. Examples are prevalent in many engineering disciplines such as transportation, robotics, energy, and biological systems. This thesis studies designing correct, resilient, and optimal controllers for discrete-time complex systems from elaborate, possibly vague, specifications. The first part of the contributions of this thesis is a framework for optimal control of non-deterministic hybrid systems from specifications described by signal temporal logic (STL), which can express a broad spectrum of interesting properties. The method is optimization-based and has several advantages over the existing techniques. When satisfying the specification is impossible, the degree of violation - characterized by STL quantitative semantics - is minimized. The computational limitations are discussed. The focus of second part is on specific types of systems and specifications for which controllers are synthesized efficiently. A class of monotone systems is introduced for which formal synthesis is scalable and almost complete. It is shown that hybrid macroscopic traffic models fall into this class. Novel techniques in modular verification and synthesis are employed for distributed optimal control, and their usefulness is shown for large-scale traffic management. Apart from monotone systems, a method is introduced for robust constrained control of networked linear systems with communication constraints. Case studies on longitudinal control of vehicular platoons are presented. The third part is about learning-based control with formal guarantees. Two approaches are studied. First, a formal perspective on adaptive control is provided in which the model is represented by a parametric transition system, and the specification is captured by an automaton. A correct-by-construction framework is developed such that the controller infers the actual parameters and plans accordingly for all possible future transitions and inferences. The second approach is based on hybrid model identification using input-output data. By assuming some limited knowledge of the range of system behaviors, theoretical performance guarantees are provided on implementing the controller designed for the identified model on the original unknown system.
RightsAttribution 4.0 International
Showing items related by title, author, creator and subject.
Gschwendter, Thomas (Boston University Computer Science Department, 2000-05-12)This thesis presents a framework for aggregated congestion management for TCP flows and shows how to integrate such an approach in an existing TCP protocol stack. The thesis presents an initial implementation of this ...
Is the Tobacco Control Movement Misrepresenting the Acute Cardiovascular Health Effects of Secondhand Smoke Exposure? An Analysis of the Scientific Evidence and Commentary on the Implications for Tobacco Control and Public Health Practice Siegel, Michael (BioMed Central, 2007-10-10)While chronic exposure to secondhand smoke has been well recognized as a cause of heart disease in nonsmokers, there has been recent speculation about the potential acute cardiovascular effects of transient exposure to ...