As robots become more prevalent, the complexity of robot-robot, robot-human, and robot-environment interactions increases. In these interactions, a robot needs to consider not only the effects of its own actions, but also the effects of other agents' actions and the possible interactions between agents. Previous works have considered reactive synthesis, where the human/environment is modeled as a deterministic, adversarial agent; as well as probabilistic synthesis, where the human/environment is modeled via a Markov chain. While they provide strong theoretical frameworks, there are still many aspects of human-robot interaction that cannot be fully expressed and many assumptions that must be made in each model. In this work, we propose stochastic games as a general model for human-robot interaction, which subsumes the expressivity of all previous representations. In addition, it allows us to make fewer modeling assumptions and leads to more natural and powerful models of interaction. We introduce the semantics of this abstraction and show how existing tools can be utilized to synthesize strategies to achieve complex tasks with guarantees. Further, we discuss the current computational limitations and improve the scalability by two orders of magnitude by a new way of constructing models for PRISM-games.

翻译：随着机器人日益普及，机器人-机器人、机器人-人类及机器人-环境交互的复杂性不断增加。在这些交互过程中，机器人不仅需要考虑自身动作的影响，还需考虑其他智能体行为的影响以及智能体之间可能的相互作用。先前的工作考虑了反应式综合（将人类/环境建模为确定性对抗智能体）和概率综合（通过马尔可夫链对人类/环境进行建模）。虽然这些方法提供了坚实的理论框架，但人机交互的许多方面仍无法完全表达，且每个模型都必须做出诸多假设。在本工作中，我们提出将随机博弈作为人机交互的通用模型，其表达能力涵盖了之前所有表示形式。此外，该模型能减少建模假设，从而产生更自然、更强大的交互模型。我们介绍了这种抽象模型的语义，展示了如何利用现有工具综合策略以实现具有保证的复杂任务。进一步地，我们讨论了当前的计算局限性，并通过一种为PRISM-games构建模型的新方法，将可扩展性提升了两个数量级。