N-ATL and ATL-G, Two Approaches for Goal Specification in Advanced Distributed Computing Systems

When specifying goals of agents, temporal logics such as linear temporal logic LTL and branching time temporal logic CTL are adopted as basic tools. In order to specify goals in view of multi-agent cooperation which is one aspect of social interaction, two logic frameworks are proposed in this paper based on alternating-time temporal logic ATL. Firstly, ATL is extended with strong and weak exceptions so as to facilitate non-monotonic reasoning of goals, and N-ATL whose model checking complexity is PTIME-complete is proposed. As far as we know, N-ATL is the first multi-agent cooperation logic that takes non-monotonic reasoning into account in the literature. Secondly, ATL is extended with goal operator which is one kind of modal operators, and ATL-G whose model checking complexity is also PTIME-complete is proposed. Examples are introduced to show the usage of these two new multi-agent cooperation logics whose properties are analyzed as well.