CGMurphi: Automatic Synthesis of Numerical Controllers for Nonlinear Hybrid Systems

In the last years, the use of controllers has become very common, thus much work is being done to create automatic controller synthesis tools. When dealing with critical systems, most of the times such controllers are required to be optimal and robust, i.e., they must achieve their goal with minimal resource consumption and be able to handle also unexpected situations. All these requirements, which are intrinsically difficult to satisfy, become even more challenging when dealing with hybrid systems, which represent a wide range of real world systems. In this paper we propose a model checking based tool, namely CGMurphi, which assists in the the generation of optimal and robust numerical controllers for systems having complex dynamics, possibly hybrid systems. The tool provides a complete controller generation solution, being also able to effectively compress the controllers and encode them so that they can be directly embedded in software/hardware systems. The tool has been widely experimented with very promising results. In particular, the present paper reports the complete experimentation results relative to two academic case studies, and the preliminary achievements obtained by applying CGMurphi to an industrial critical system.