Correct-by-Construction Control Adaptation against Sensing, Model, and Information Uncertainty

The theory of Formal Methods had a profound effect on the world of Computer Science by providing tools that generate software that is “correct-by-construction” (among other things). Correct, bug-free code is not only helpful in pure software systems, but also in systems that interact with and manipulate the world (Cyber-Physical Systems, CPSs). Unfortunately, there are limitations that prevent Formal Methods from being applied to many CPSs including sensing, modeling and information uncertainty. In this thesis, I discuss several approaches for incorporating these uncertainties while formally guaranteeing satisfaction of the tasks at hand. The tasks that I am interested in are discrete-time reachability and safety (I.e., invariance), which I approach using tools from convex optimization and fixed-point computation of convex sets. I use these algorithms to show how correct and safe control can be done (i) when sensor packet drops occur during control operation, (ii) when there is uncertainty in what the correct model of the system is or (iii) when the controller is for a single agent in a “team” of which it only has partial information about.

Chair: Professor Necmiye Ozay