Automatic generation of optimal controllers through model checking techniques