Automated synthesis of safe and robust PID controllers for stochastic hybrid systems

We present a new method for the automated synthesis of safe and robust PID controllers for stochastic hybrid systems such that the resulting closed-loop system satisfies a given probabilistic reachability specification. Proportional-Integral-Derivative (PID) control is the most common feedback-control technique found in industry, and is used in a variety of applications ranging from process control to flight control. While well-established for linear systems, the synthesis of PID controllers is generally more difficult for nonlinear systems, especially those that exhibit stochastic and hybrid dynamics. Our approach is unique in that it supports stochastic hybrid systems with general nonlinear dynamics (Lipschitz-continuous ordinary differential equations) and random parameters, while ensuring that the synthesized controller satisfies the specification with formal guarantees. In particular we aim at solving two complementary problems: 1) synthesize a controller that minimizes the probability of violating the specification; 2) for a given controller, synthesize the maximum disturbance that can be supported by the closed-loop system. The synthesis algorithm is built on top of a probabilistic extension of decision procedures for satisfiability modulo theories (SMT) solving over the reals with ODEs. We demonstrate the utility of our approach on the problem of insulin regulation for type~1 diabetes. In particular, we synthesize controllers able to provide robust responses to large random meal disturbances, while keeping the system within healthy, safe blood glucose ranges.