Reasoning about belief, goal and exceptions in multi-agent cooperation logics

When specifying mental states such as belief and goal of agents, temporal logics are often adopted as basic tools. Although there are work on non-monotonic extension of linear temporal logic LTL and branching time temporal logic CTL, the non-monotonic extension of alternating-time temporal logic ATL which is an important kind of multi-agent cooperation logics has not been discussed yet in literature. To solve this problem, this paper proposed non-monotonic alternating-time temporal logic with belief and goal, namely N-ATL-GB to facilitate the non-monotonic reasoning of mental states of agents. Firstly, concurrent game structures of ATL are extended by strong and weak exceptions, two kinds of modal operators are introduced into the syntax of N-ATL-GB, and exceptions removing model is built. Secondly, the corresponding model checking algorithm which can be finished in polynomial time is proposed. Examples are given to show the usage of this new logic at last.