Automated Generation of Optimal Controllers through Model Checking Techniques

We present a methodology for the synthesis of controllers, which exploits

(explicit) model checking techniques

. That is, we can cope with the systematic exploration of a very large state space. This methodology can be applied to systems where other approaches fail. In particular, we can consider systems with an

highly non-linear dynamics

and

lacking a uniform mathematical description (model)

. We can also consider situations where the required control action cannot be specified as a local action, and rather a kind of

planning

is required. Our methodology individuates first a raw optimal controller, then extends it to obtain a more robust one. A case study is presented which considers the well known

truck-trailer obstacle avoidance parking problem

, in a parking lot with

obstacles

on it. The complex non-linear dynamics of the truck-trailer system, within the presence of obstacles, makes the parking problem extremely hard. We show how, by our methodology, we can obtain optimal controllers with different degrees of robustness.