Formal Specification of Multi-Agent Systems: a Real World Case

Abstract

In this paper the framework DESIRE, originally designed for formal specification of complex reasoning systems is used to specify a real-world multi-agent application on a conceptual level. Some extensions to DESIRE are introduced to obtain a useful formal specification framework for multi-agent systems. 1 Introduction In many areas of software engineering and knowledge-based system design, formal specifications of the conceptual design of complex systems are devised before systems are implemented; for an overview in the area of complex (knowledge-based) reasoning systems, see (Treur & Wetter 93). Such specifications describe the semantics of systems without concern for implementation details, providing a basis for verification and validation of the functionality of the systems. Most specification frameworks, however, do not provide adequate means to describe the dynamics of reasoning behaviour and acting behaviour (e.g., guided reasoning, observation, communication and execution of ac...