Compositionally analyzing a proportional-integral controller family

We define always eventually region stability and then formulate the absolute always eventually region stability problem as the problem of finding a class of plants that a generic proportional-integral (PI) controller can always eventually stabilize. We use real quantifier elimination methods to solve the absolute always eventually region stability problem. The class of plants found in our solution includes nonlinear and switched plant models. Our analysis reveals that if a PI controller satisfies two assumptions of the form: (a) the proportional gain Kp and the integral gain Ki satisfy an inequality, and (b) the integral of the error term in the controller is saturated, then such a PI controller can be used to establish always eventually region stability for any plant that suitably responds to the control input. Such a result is useful for compositionally verifying a system consisting of a plant and a controller.