Discrete event models+temporal logic=supervisory controller: automatic synthesis of locomotion controllers