Automated Verification of Goal Net Models

Multi-agent systems are increasingly complex and the problem of their verification is acquiring increasing importance. Most of the existing approaches are based on model checking techniques which require system specification in a formal language. This is an error-prone task and can only be performed by experts who have considerable experiences in logic reasoning. We proposed in this paper an easy-to-use approach to the verification of multi-agent systems based on the Goal Net modeling methodology. Goal Net is a goal-oriented framework which aspires to simplify the process of designing and implementing multi-agent systems. In our approach, a multi-agent system is modeled as a goal net. The goal net and its properties will be automatically converted into FSP (Finite State Processes) specification, which can be automatically verified by the model checker LTSA (Labeled Transition System Analyzer).