In: Ricardo Choren, Alessandro Garcia, Carlos Lucena, et al. (Eds.): Lecture Notes in Computer Science, Vol. 3390: Software Engineering for Multi-Agent Systems III: Research Issues and Practical Applications, pages 162-179. Springer-Verlag, 2005.
Abstract: Multiagent systems are characterized by decentralized control and agents that perform autonomous actions. The sequence of such actions are generally described by plans. An important issue in this context is how to verify the correctness of plans when agents have unpredicted actions. In this paper, formal modelling and verification guidelines to verify nondeterministic multiagent system plans are introduced. The guidelines are based on HCPN modelling, simulation, and model checking. The guidelines are conceptually introduced, and then applied for a multiagent intelligent tutoring system modelling and verification.