Abstract
Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be lifted to be applicable to multiagent systems. Our approach allows us to reuse the technology and tools developed in model checking, to design and verify multiagent systems in a modular and incremental way, and also to have a very efficient model checking algorithm.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. E. Bratman. Intention, plan and practical reason. Harvard University Press, 1990.
E. Clarke, O. Grumberg, and D. Long. Model Checking. In Deductive Program Design (Manfred Broy, ed.), NATO ASI Series, Springer-Verlag (1995), pages 305–349. Proceedings of the NATO Advanced Study Institute on Deductive Program Design, held in Marktoberdorf, Germany (1994).
J. Engelfriet, C. M. Jonker, and J. Treur. Compositional verification of multi-agent systems in temporal multi-epistemic logic. In J. P. Müller, M. P. Singh, and A. S. Rao, editors, Intelligent Agents V — Proceedings of the Fifth International Workshop on Agent Theories, Architectures, and Languages (ATAL-98), Lecture Notes in Artificial Intelligence. Springer-Verlag, Heidelberg, 1999. In this volume.
FIPA Foundation for Intelligent Physical Agents. Fipa’ 97 draft specification, 1997. Revision 2.0 available at http://drogo.cselt.stet.it/fipa/.
E. Giunchiglia and F. Giunchiglia. Ideal and Real Belief about Belief. In Practical Reasoning, International Conference on Formal and Applied Practical Reasoning, FAPR’96, number 1085 in Lecture Notes in Artificial Intelligence, pages 261–275. Springer Verlag, 1996.
O. Grumberg, editor. Proceedings of the 9th International Conference on Computer-Aided Verification, CAV’97, Haifa, Israel, 1997. Springer Verlag.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.
A. S. Rao and M. P. Georgeff. Modeling rational agents within a BDI architecture. In J. Allen, R. Fikes, and E. Sandewall, editors, Proceedings of the 2nd International Conference on Principle of Knowledge Representation and Reasoning, pages 473–484. Morgan Kaufmann, 1991.
A. S. Rao and M. P. Georgeff. A model-theoretic approach to the verification of situated reasoning systems. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), pages 318–324, Chambéry, France, 1993.
K. Schild. On the relationship between BDI logics and standard logics of concurrency. In J. P. Müller, M. P. Singh, and A. S. Rao, editors, Intelligent Agents V — Proceedings of the Fifth International Workshop on Agent Theories, Architectures, and Languages (ATAL-98), Lecture Notes in Artificial Intelligence. Springer-Verlag, Heidelberg, 1999. In this volume.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benerecetti, M., Giunchiglia, F., Serafini, L. (1999). A Model Checking Algorithm for Multi-agent Systems. In: Müller, J.P., Rao, A.S., Singh, M.P. (eds) Intelligent Agents V: Agents Theories, Architectures, and Languages. ATAL 1998. Lecture Notes in Computer Science, vol 1555. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49057-4_11
Download citation
DOI: https://doi.org/10.1007/3-540-49057-4_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65713-2
Online ISBN: 978-3-540-49057-9
eBook Packages: Springer Book Archive