Temporal logic planning for mobile robots