A Framework for the Formal Analysis of Multi-Agent Systems

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 2003
Accession Number
ADA465311

Entities

People

  • Ramesh Bharadwaj

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Cyber

DTIC Thesaurus Topics

  • Automata
  • Computer Programming
  • Computers
  • Environment
  • Information Operations
  • Information Systems
  • Invariance
  • Language
  • Machines
  • Military Research
  • Multiagent Systems
  • Notation
  • Programming Languages
  • Security
  • Software Agents
  • Transitions
  • Unmanned Systems

Fields of Study

  • Computer science

Readers

  • Agent-Based Social Robotics and Mobile-Assisted Learning in Virtual Environments.
  • Distributed Systems and Data Platform Development
  • Mathematical Modeling and Probability Theory.