Open-world mission specification for reactive robots

Recent advances have enabled the automatic generation of correct-by-construction robot controllers from high-level mission specifications. However, most current approaches operate under the closed-world assumption, i.e., only elements of the world explicitly modeled a priori can be taken into account during execution. In this paper, we tackle the problem of specifying and automatically updating the missions of robots operating in worlds that are open with respect to new elements, such as new objects and regions of interest. We demonstrate our approach in a scenario featuring a robotic courier whose world is open with respect to letters addressed to new recipients.