Execution and analysis of high-level tasks with dynamic obstacle anticipation

This paper uniquely embeds high-level robot controllers with sensor data obtained from abstracting probabilistic anticipation of the behavior of dynamic obstacles. An example problem of an autonomous vehicle operating in an urban environment, in the presence of other vehicles and pedestrians, is used as motivation. The correct-by-construction controller is automatically synthesized from a set of high-level tasks, specified as temporal logic formulas. The anticipated behavior of other vehicles is abstracted to a set of propositions describing the safety of road segments at intersections, and used as the output of high-level sensors for the controller. Such an input to the controller is inherently probabilistic, and this paper investigates the types of probabilistic guarantees that can be made about the system using both formal and statistical analysis.