Multi-agent Belief,Goal and Exceptions Reasoning

Temporal logics are often adopted as basic tools to specifying mental states such as belief and goal of agents. Although there are works 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-BG,to facilitate the non-monotonic reasoning of mental states of agents. The semantic model,syntax and semantics of this new logic are developed. A model checking algorithm which can be finished in polynomial time is proposed for this new logic. Examples are given to show its usage.