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.

翻译：本文提出了面向定量反应综合的高效符号化算法。我们考虑资源受限的机械臂，其需与人类交互以完成用线性时序逻辑表达的复杂任务。我们的框架生成的反应策略不仅保证任务完成，还尽可能寻求与人类的合作。我们将交互建模为双人博弈，并采用最小化遗憾策略以促进合作。通过符号化表示博弈状态实现可扩展性。在综合过程中，我们首先针对此类具有最小最大目标的博弈引入值迭代算法，随后将方法扩展至最小化遗憾目标。基准测试表明，我们的符号化框架不仅显著提升计算时间（最高可达一个数量级），还能将操纵问题的可解规模扩展至先前方法的两倍（物体与位置数量）。