Abstract
Verification of multi-agent systems is a challenging task due to their dynamic nature, and the complex interactions between agents. An example of such a system is the RoboCup Soccer Simulator, where two teams of eleven independent agents play a game of football against each other. In the present article we attempt to verify a number of properties of RoboCup football teams, using a methodology involving testing. To accomplish such testing in an efficient manner we use the McErlang model checker, as it affords precise control of the scheduling of the agents, and provides convenient access to the internal states and actions of the agents of the football teams.
This work has been partially supported by the FP7-ICT-2007-1 project ProTest (215868), a Ramón y Cajal grant from the Spanish Ministerio de Educación y Ciencia, and the Spanish national projects TRA2007-67374-C02-02, TIN2006-15660-C02-02 (DESAFIOS) and S-0505/TIC/0407 (PROMESAS).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang. Prentice-Hall, Englewood Cliffs (1996)
Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. Autonomous Agents and Multi-Agent Systems 12(2), 239–256 (2006)
Bosse, T., Lam, D.N., Barber, K.S.: Automated analysis and verification of agent behavior. In: AAMAS 2006: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, pp. 1317–1319. ACM Press, New York (2006)
Chen, M., Dorer, K., Foroughi, E., Heintz, F., Huang, Z., Kapetanakis, S., Kostiadis, K., Kummeneje, J., Murray, J., Noda, I., Obst, O., Riley, P., Steffens, T., Wang, Y., Yin, X.: RoboCup Soccer Server (2003); Manual for Soccer Server Version 7.07 and later (obtainable from sserver.sf.net)
Fredlund, L.: Implementing WS-CDL. In: Proceedings of the second Spanish workshop on Web Technologies (JSWEB 2006). Universidade de Santiago de Compostela (November 2006)
Fredlund, L., Svensson, H.: McErlang: a model checker for a distributed programming language. In: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming (2007)
Furbach, U., Murray, J., Schmidsberger, F., Stolzenburg, F.: Model checking hybrid multiagent systems for the roboCup. In: Visser, U., Ribeiro, F., Ohashi, T., Dellaert, F. (eds.) RoboCup 2007: Robot Soccer World Cup XI. LNCS, vol. 5001, pp. 262–269. Springer, Heidelberg (2008)
Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Torstendahl, S.: Open telecom platform. Ericsson Review 1 (1997)
Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification, pp. 332–344 (1986)
Visser, W., Havelund, K., Brat, G., Park, S.: Java pathfinder - second generation of a java model checker (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benac Earle, C., Fredlund, LÅ., Iglesias, J.A., Ledezma, A. (2009). Verifying Robocup Teams. In: Peled, D.A., Wooldridge, M.J. (eds) Model Checking and Artificial Intelligence. MoChArt 2008. Lecture Notes in Computer Science(), vol 5348. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00431-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-00431-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00430-8
Online ISBN: 978-3-642-00431-5
eBook Packages: Computer ScienceComputer Science (R0)