A First-Order Branching Time Logic OF MULTI-AGENT SYSTEMS
Michael Wooldridge, Michael Fisher · 1992
This paper presents a first-order branching time temporal logic that is suitable for describing and reasoning about a wide class of computational multi-agent systems. The logic is novel in that it supports reasoning about the beliefs, actions, goals, abilities and structure of groups of agents. A sound proof system for the logic is presented, and some short examples are given, showing how the logic might be used to specify desirable properties of multi-agent systems. 1 Introduction This paper presents a logic that is suitable for describing and reasoning about multi-agent systems (MAS). We take a MAS to be one composed of a number of computational entities built along the lines of classical AI research, which communicate through point-to-point message passing. Our strategy is to construct an abstract formal theory of MAS, and then build a logic corresponding to this theory [Wooldridge, 1992] . Our theory of MAS is in the spirit of [Konolige, 1986] , in that it is explicitly architectu...