A Framework for the Formal Analysis of Multi-Agent Systems
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
Pagination or Media Count:
In this paper we present an integrated formal framework for the specification and analysis of Multi-Agent Systems MAS. Agents are specified in a synchronous programming language called Secure Operations Language SOL which supports the modular development of secure agents. Multi-agent systems are constructed from individual agent modules by using the composition operator of SOL, the semantics of which are guaranteed to preserve certain individual agent properties. The formal semantics and the underlying framework of SOL also serve as the basis for analysis and transformation techniques such as abstraction, consistency checking, verification by model checking or theorem proving, and automatic synthesis of agent code. Based on this framework, we are currently developing a suite of analysis and transformation tools for the formal specification, analysis, and synthesis of multi-agent systems.
- Computer Programming and Software
- Computer Systems Management and Standards