Analyzing and revising high-level robot behaviors under actuator error

One increasingly popular approach for creating robot controllers for complex tasks is to automatically synthesize a hybrid controller from a high-level task specification. Such an approach, in addition to reducing the time and expertise required for creating a controller, guarantees that the robot will satisfy all of the underlying specifications, given perfect sensing and actuation. This paper investigates the probabilistic guarantees that can be made about the behavior of the robot when the actuation of the robot is no longer assumed to be perfect, as well as the possible specification revisions that can be made to improve the behavior of the robot. The approach described in this paper composes probabilistic models of the environment behavior and the robot actuation error with the synthesized controller, and uses probabilistic model checking techniques to find the probability that the robot satisfies a set of high level specifications. This paper also presents a preliminary approach for analyzing the composed model and automatically generating revisions to improve the robot´s high-level behavior.