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.

翻译：本文介绍了用于定量反应式综合的高效符号算法。我们考虑资源受限的机械臂，其需要与人类交互以完成用线性时序逻辑表达的复杂任务。我们的框架生成不仅保证任务完成，而且在可能时寻求与人类合作的反应式策略。我们将交互建模为双人博弈，并采用最小遗憾策略来促进合作。我们使用博弈的符号表示以实现可扩展性。对于综合问题，我们首先引入了针对此类具有最小-最大目标的博弈的值迭代算法。然后，我们将方法扩展到最小遗憾目标。我们的基准测试表明，我们的符号框架不仅显著提高了计算时间（最高可达一个数量级），而且能够扩展到比现有技术多两倍物体和位置数量的更大规模操作问题实例。