Synthesizing cooperative reactive mission plans

By performing synthesis from formal high-level mission specifications, we can obtain robot controllers that are guaranteed to operate correctly under the specified environment conditions. Such conditions must be stated in the specification whenever there is no way in which the robot´s task can be fulfilled without them holding, and they relate the possible behaviors of the environment with the behavior of the robot. Contemporary synthesis algorithms however frequently construct implementations that try to trivially satisfy their specifications by actively working towards the violation of the assumptions, which is undesirable behavior.