Analyzing and revising synthesized controllers for robots with sensing and actuation errors

摘要

The synthesis of verifiable robot controllers from a set of high-level task specifications provides a valuable tool for creating robot controllers for complex tasks. Such an approach can offer a number of advantages over more traditional programming methods, including the guarantee that the synthesized controller will satisfy all of its underlying specifications when operating with perfect sensing and actuation. This paper relaxes that assumption, and describes a method for probabilistically analyzing the behavior of a robot controller that is synthesized from a set of temporal logic specifications, when the robot operates with uncertainty in its sensing and actuation. The described approach creates a probabilistic model of the system and uses probabilistic model checking techniques to find the probability that it satisfies some set of specifications. In addition, the paper proposes a method which leverages that analysis to provide automated feedback to the user in the form of suggested revisions to the task specification or low-level components, in order to increase the probability that the robot successfully accomplishes its task.