MULTI AGENT PLAN VERIFICATION

Abstract

Multi-agent systems are characterized by decentralized control and self-independent agents that perform autonomous actions. A sequence of such actions is usually described by plans. An important issue that arises now is how to verify the correctness of plans when the actions become unpredictable. In this dissertation, we have demonstrated the use of model-checking techniques for the formal verification of such multi-agent system plans. Interesting properties in these plans are observed and identified and their specification requirements are expressed in temporal logics (CTL/LTL).Model checking tools such as UPPAAL and SPIN have then been used to model, analyze, and verify plans in a multi agent scenario. Thus a given plan trajectory, in which the agents move from a set of initial positions to a set of desired goal positions, may be analyzed and verified for its correctness