Automatic Synthesis of Stabilizing Controllers for Discrete Time Linear Hybrid Systems

Many Cyber-Physical Systems are either mission or safety critical, thus the controllers for such systems must be provably correct. To this aim, in the last decades many methodologies have been developed which are able to automatically generate correct-by-construction controllers for Cyber-Physical Systems. In this paper, we focus on one of such methodologies, implemented in the QKS tool, which is able to explicitly take into account the specification of the discretization of the state space due to analog-todigital conversion. Controllers output by QKS are able to drive any controllable state inside the system goal. However, such controllers may allow a goal state to go outside the goal region, in order to be able to bring it back into the goal region later. QKS does not provide any means to detect such behavior. Here we propose to modify QKS in order to provide an additional feature, which only outputs stabilizing controllers, i.e., controllers which never allow goal states to go outside the goal region. If this is not possible for the input system, an empty controller is returned. We prove the feasibility of our approach on well-known control theory case studies, namely the multi input buck DC-DC converter and the inverted pendulum. Our experimental results show that we are able to output stabilizing controllers using limited additional resources with respect to the original QKS. c 2021