Real-life agents seldom have unlimited reasoning power. In this paper, we propose and study a new formal notion of computationally bounded strategic ability in multi-agent systems. The notion characterizes the ability of a set of agents to synthesize an executable strategy in the form of a Turing machine within a given complexity class, that ensures the satisfaction of a temporal objective in a parameterized game arena. We show that the new concept induces a proper hierarchy of strategic abilities -- in particular, polynomial-time abilities are strictly weaker than the exponential-time ones. We also propose an ``adaptive'' variant of computational ability which allows for different strategies for each parameter value, and show that the two notions do not coincide. Finally, we define and study the model-checking problem for computational strategies. We show that the problem is undecidable even for severely restricted inputs, and present our first steps towards decidable fragments.
翻译:现实世界中的智能体很少拥有无限的推理能力。本文提出并研究多智能体系统中计算受限策略能力的新形式概念。该概念刻画了一组智能体在给定复杂度类内,以图灵机形式合成可执行策略的能力,从而在参数化博弈舞台中确保时序目标的满足。研究表明,新概念会诱导出策略能力的层级结构——特别地,多项式时间能力严格弱于指数时间能力。本文还提出计算能力的"自适应"变体,该变体允许不同参数值对应不同策略,并证明这两种概念并不等价。最后,我们定义并研究计算策略的模型检测问题。研究表明,即使对严重受限的输入,该问题仍不可判定,并提出可判定子问题的初步研究成果。