Abstract Formal methods - mathematical techniques for describing systems, capturing requirements, and providing guarantees - have been used to synthesize robot control from high-level specification, and to verify robot behavior. […]