Abstract
This paper presents mcmas, a model checker for Multi-Agent Systems (MAS). Differently from traditional model checkers, mcmas permits the automatic verification of specifications that use epistemic, correctness, and cooperation modalities, in addition to the standard temporal modalities. These additional modalities are used to capture properties of various scenarios (including communication and security protocols, games, etc.) that may be difficult or unnatural to express with temporal operators only; a small number of applications are presented in Section[4]. Agents are described in mcmas by means of the dedicated programming language ISPL (Interpreted Systems Programming Language). The approach is symbolic and uses ordered binary decision diagrams (obdds), thereby extending standard techniques for temporal logic to other modalities distinctive of agents. mcmas and all the examples presented in this paper are available for download [14] under the terms of the GPL license.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672–713 (2002)
Bordini, R., Fisher, M., Pardavila, C., Visser, W., Wooldridge, M.: Model checking multiagent programs with CASP. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 110–113. Springer, Heidelberg (2003)
Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1(1), 65–75 (1988)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)
van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: Gini, M., Ishida, T., Castelfranchi, C., Johnson, W.L. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), pp. 1167–1174. ACM Press, New York (2002)
Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundamenta Informaticae 62, 1–35 (2004)
Jonker, G.: Feasible strategies in alternating-time temporal epistemic logic. Master’s thesis, University of Utrech, The Netherlands (2003)
Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica 75(1), 63–92 (2003)
Lomuscio, A., Sergot, M.: A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic 2(1), 93–116 (2004)
Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M.: VerICS 2004: A model checker for real time and multi-agent systems. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2004). Informatik-Berichte, vol. 170, pp. 88–99. Humboldt University (2004)
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185
Raimondi, F., Lomuscio, A.: MCMAS - A tool for verification of multi-agent systems, http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/
Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic (2005); To appear in Special issue on Logicbased agent verification
Somenzi, F.: CUDD: CU decision diagram package - release 2.4.0, http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lomuscio, A., Raimondi, F. (2006). mcmas: A Model Checker for Multi-agent Systems. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_31
Download citation
DOI: https://doi.org/10.1007/11691372_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)