Model-checking of distributed autonomous agents using logic programming

Systems of autonomous agents providing automated services over the Web are fast becoming a reality. Often these multi-agent systems (MAS) are constructed using procedural architectures providing a framework for connecting agents that perform specific tasks. The designer codes the tasks for each agent and uses the framework to connect the agents into a MAS. The Cougaar Cognitive Agent Architecture is an example of such a framework. This approach does not provide easy verification of global properties of constructed agent systems. An alternate approach to building MAS describes the agent system in a declarative language that directly translates to a logical model. Languages such as AgentSpeak, based on the semantics of the Belief-Desire-Intention (BDI) paradigm for describing agents, use this approach. This approach allows for easy verification of logical properties of the MAS, but requires that the logical model be implemented using a special purpose interpreter or compiler. Also fault tolerance and inter-agent communications are not addressed by declarative agent languages. Frameworks like Cougaar incorporate these features in the framework infrastructure so that the designer can assume a certain level of service.; I outline here a methodology based on logic programming for modeling procedural agent frameworks using the Cougaar Architecture as an example. This methodology directly translates Cougaar systems into a state transition system. I then show how global properties of a Cougaar system can be specified as temporal logic formulae and outline a GCTL* temporal logic model checker which can be used to verify these properties. Within the community studying MAS, BDI logic is the preferred logic for expressing properties of MAS. This is a multi-modal logic which adds modalities for beliefs, desires, and intentions to CTL* logic. I also show how the GCTL* model checking system can be extended to BDI logic. The BDI extension to the model checker allows for direct verification of BDI logic properties of an MAS. I contrast BDI models to Cougaar models and suggest ways in which they may be integrated. Finally, I present a four agent Cougaar system for resource bound order processing and illustrate some verified properties of this system.