Date/Time: 21st of November 2017, 13:00-14:00

Venue: CBCB Baddiley-Clark Building, large meeting room level 2

Abstract:

We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems, and we apply it to an Artificial Pancreas model. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for stochastic hybrid systems. In particular, we consider hybrid systems with nonlinear differential equations and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for Type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.

 

Biography:

Dr. Paolo Zuliani is a Senior Lecturer in the School of Computing at Newcastle University. He received his Laurea degree in computer science from Universita' degli Studi di Milano, Italy, and his DPhil in computer science from the University of Oxford, UK. Dr. Zuliani's expertise lies largely in formal methods for reasoning about computing systems, with an emphasis on probabilistic systems. He is in particular interested in the verification of biological systems and cyber-physical systems.