Modeling Cooperative Problem Solving Process with Extended Alternating-time Temporal Logic

The paradigm example of social interaction is cooperative problem solving, in which a group of autonomous agents choose to work together to achieve a common goal. In order to improve existing work on developing formal computing model for cooperative problem solving in multi-agent systems, several efforts are made in this paper. Firstly, a new multi-agent cooperation logic called ATI-BDI designed in our previous work is enhanced so as to make it more suitable for modeling cooperative problem solving. Secondly, basing on ATI-BDI, the cooperative problem solving process is formally described. The corresponding new computing models of cooperation recognition, team formation, plan formation and execution are developed. The iteration of these steps is also well considered. Several important properties are gained and proved finally.