Automatic Synthesis of Robust Numerical Controllers

A major problem of numerical controllers is their robust-ness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an in-novative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most sig-nificant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurϕ tool, an extension of the well-known CMurϕ verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem.