Translating temporal logic to controller specifications