Tech Reports

ULCS-09-021

Verification of Multi-agent Systems via Combined Model Checking

Savas Konur, Michael Fisher and Sven Schwe

Abstract

Model checking is a well-established technique for the formal verification of concurrent and distributed systems. In recent years, model checking has been extended and adapted for use in multi-agent systems, primarily to enable the formal analysis of BDI systems. While this has been successful, there is a need for more complex logical frameworks in order to verify realistic multi-agent systems. In particular, probabilistic and real-time aspects, as well as knowledge, belief, goals, etc., are required.

However, the development of new model checking tools for complex combinations of logics is both difficult and time consuming. In this paper, we show how model checkers for the constituent logics can be re-used in a modular way when we consider combined logics involving different dimensions. This avoids the re-implementation of model checking procedures. Within this work we define a modular approach, prove its correctness, establish its complexity, and show how it can be used to describe existing combined approaches.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.