CGMurphi

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 {it optimal} and {it 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 {it hybrid systems}, which represent a wide range of real world systems.par In this paper we propose a model checking based tool, namely CGMurphi, which assists in 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.par 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.