@conference {61, title = {Provably Correct Continuous Control for High-Level Robot Behaviors with Actions of Arbitrary Execution Durations}, booktitle = {2013 IEEE International Conference on Robotics and Automation}, year = {2013}, month = {05/2013}, publisher = {IEEE press}, organization = {IEEE press}, address = {Karlsruhe, Germany}, abstract = {Formal methods have recently been successfully applied to the construction of verifiable high-level robot con- trol. Most approaches use a discrete abstraction of the un- derlying continuous domain, and make simplifying assump- tions about the physical execution of actions given a discrete implementation. Relaxing these assumptions gives rise to a number of challenges in the continuous implementation of automatically-synthesized hybrid controllers. This paper de- scribes a controller-synthesis framework that ensures correct continuous behaviors by explicitly modeling the activation and completion of the continuous low-level controllers. The synthe- sized controllers exhibit desired properties including immediate reactiveness to sensor events and guaranteed safety of physical executions, and the approach extends to any number of robot actions with arbitrary relative timings.}, author = {Vasumathi Raman and Nir Piterman and Hadas Kress-Gazit} }