Automated verification of resource requirements in multi-agent systems using abstraction

N. Alechina, B. Logan, H.N. Nguyen, A. Rakib

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

6 Citations (Scopus)


We describe a framework for the automated verification of multi-agent systems which do distributed problem solving, e.g. query answering. Each reasoner uses facts, messages and Horn clause rules to derive new information. We show how to verify correctness of distributed problem solving under resource constraints, such as the time required to answer queries and the number of messages exchanged by the agents. The framework allows the use of abstract specifications consisting of Linear Time Temporal Logic (LTL) formulas to specify some of the agents in the system. We illustrate the use of the framework on a simple example.
Original languageEnglish
Title of host publicationModel Checking and Artificial Intelligence
Number of pages16
ISBN (Electronic)978-3-642-20674-0
ISBN (Print)978-3-642-20673-3
Publication statusPublished - 2011
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • model check
  • atomic formula
  • user agent
  • linear time temporal logic
  • datalog program


Dive into the research topics of 'Automated verification of resource requirements in multi-agent systems using abstraction'. Together they form a unique fingerprint.

Cite this