Cătălin Dima
Université Paris-Est Créteil, France

Real-life agents seldom have unlimited reasoning power. In this talk, 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 linear temporal logic formula 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. Talk based on joint work with Wojtek Jamroga.