Alternating-time Temporal Epistemic Logic (ATEL) which is an important kind of multi-agent cooperation logics only takes knowledge into account,but does not deal with belief of agents. By introducing three kinds of be...Alternating-time Temporal Epistemic Logic (ATEL) which is an important kind of multi-agent cooperation logics only takes knowledge into account,but does not deal with belief of agents. By introducing three kinds of belief operators into ATEL,a new multi-agent cooperation logic named ATBKL (Alternating-time Temporal Belief and Knowledge Logic) was developed. A model checking algorithm was proposed. It is proved that the model checking complexity of ATBKL is the same as that of ATEL,i.e.,the presented logic is better for further study of multi-agent systems.展开更多
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 tem...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.展开更多
基金Natural Science Foundation of Fujian Province of China ( No.2006J0316)College Scientific and Technological Projects of Office of Education of Fujian Province of China (No.JB09302)Scientific Research Foundation for Young Teachers of Fujian Agriculture and Forestry University,China (No.08B21)
文摘Alternating-time Temporal Epistemic Logic (ATEL) which is an important kind of multi-agent cooperation logics only takes knowledge into account,but does not deal with belief of agents. By introducing three kinds of belief operators into ATEL,a new multi-agent cooperation logic named ATBKL (Alternating-time Temporal Belief and Knowledge Logic) was developed. A model checking algorithm was proposed. It is proved that the model checking complexity of ATBKL is the same as that of ATEL,i.e.,the presented logic is better for further study of multi-agent systems.
基金Natural Science Foundation of Fujian Province of China ( No.2006J0316)College Scientific and Technological Project of Office of Education of Fujian Province of China ( No.JB09302)Scientific Research Foundation for Young Teachers ofFujian Agriculture and Forestry University, China (No.08B21)
文摘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.
