Alternating-time temporal belief and knowledge logic in multi-agent systems

Multi-agent cooperation logics, which provide powerful tool for modeling knowledge-based systems and cooperative problem solving process, gained great research interest in multi-agent systems community in the last five years. ATEL (alternating-time temporal epistemic logic) which is an important kind of multi-agent cooperation logics only takes knowledge into account, but does not deal with belief of agents. To solve this problem, firstly, general concurrent game structures are developed by extending concurrent game structures. Secondly, by introducing three kinds of belief operators into ATEL, a new multi-agent cooperation logic named ATBKL (alternating-time temporal belief and knowledge logic) is developed. Thirdly, a model checking algorithm is presented, and it is proved that the model checking complexity of ATBKL is PTIME-complete. Lastly, several desired properties of ATBKL are gained and proved. As a result, an expressive and powerful tool is developed for knowledge-based systems modeling. Further research is undertaken to model cooperative problem solving process based on this new logic.