Towards Formal Methods for Agent-Based Systems

This paper considers how formal methods might be developed for use in agent-based systems. In particular, it presents an approach based upon the description of agents using temporal specifications. Not only can these specifications be executed directly to provide the behaviour of an individual agent, but collections of such descriptions can be executed under a specific operational model in order to give the behaviour of multi-agent systems. In addition to animating their behaviour, verification of the agent descriptions with respect to required logical properties can be carried out; the paper outlines how temporal belief logics can be used to achieve this. Finally, the current limitations of this work are considered and its extension towards the ultimate goal of a full formal development framework for agent-based systems is discussed.