Provably Correct Continuous Control for High-Level Robot Behaviors with Actions of Arbitrary Execution Durations

TitleProvably Correct Continuous Control for High-Level Robot Behaviors with Actions of Arbitrary Execution Durations
Publication TypeConference Paper
Year of Publication2013
AuthorsRaman, V, Piterman, N, Kress-Gazit, H
Conference Name2013 IEEE International Conference on Robotics and Automation
Date Published05/2013
PublisherIEEE press
Conference LocationKarlsruhe, Germany
AbstractFormal 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.
Work Package: 
WP4