@inbook{76df5416ceca4760a8c0ea7e6f75bc24,
title = "Automated verification of resource requirements in multi-agent systems using abstraction",
abstract = "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.",
keywords = "model check, atomic formula, user agent, linear time temporal logic, datalog program",
author = "N. Alechina and B. Logan and H.N. Nguyen and A. Rakib",
year = "2011",
doi = "10.1007/978-3-642-20674-0_5",
language = "English",
isbn = "978-3-642-20673-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "69--84",
booktitle = "Model Checking and Artificial Intelligence",
address = "United Kingdom",
}