Automated Generation of Optimal Controllers through Model Checking Techniques