A linguistic method for robot verification programming and control