  This work introduces efficient symbolic algorithms for quantitative reactive
synthesis. We consider resource-constrained robotic manipulators that need to
interact with a human to achieve a complex task expressed in linear temporal
logic. Our framework generates reactive strategies that not only guarantee task
completion but also seek cooperation with the human when possible. We model the
interaction as a two-player game and consider regret-minimizing strategies to
encourage cooperation. We use symbolic representation of the game to enable
scalability. For synthesis, we first introduce value iteration algorithms for
such games with min-max objectives. Then, we extend our method to the
regret-minimizing objectives. Our benchmarks reveal that our symbolic framework
not only significantly improves computation time (up to an order of magnitude)
but also can scale up to much larger instances of manipulation problems with up
to 2x number of objects and locations than the state of the art.
