{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:23:56Z","timestamp":1775053436110,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,2,24]],"date-time":"2006-02-24T00:00:00Z","timestamp":1140739200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2006,3]]},"DOI":"10.1007\/s10458-006-5955-7","type":"journal-article","created":{"date-parts":[[2006,2,24]],"date-time":"2006-02-24T03:42:51Z","timestamp":1140752571000},"page":"239-256","source":"Crossref","is-referenced-by-count":108,"title":["Verifying Multi-agent Programs by Model Checking"],"prefix":"10.1007","volume":"12","author":[{"given":"Rafael H.","family":"Bordini","sequence":"first","affiliation":[]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,2,24]]},"reference":[{"key":"5955_CR1","first-page":"997","volume-title":"Handbook of theoretical computer science","author":"E. Allen Emerson","year":"1990"},{"key":"5955_CR2","unstructured":"Benerecetti, M., & Cimatti, A. Symbolic model checking for multi-agent systems. In Proceedings of the model checking and artificial intelligence workshop (MoChArt-2002), held with 15th ECAI, 21\u201326 July, Lyon, France, (pp. 1\u20138)."},{"key":"5955_CR3","unstructured":"Biesiadecki, J., Maimone, M. W., & Morrison, J. (2001). The Athena SDM rover: A testbed for marsrover mobility. In Sixth international symposium on AI, robotics and automation in space (ISAIRAS-01), June, Montreal, Canada."},{"key":"5955_CR4","doi-asserted-by":"crossref","unstructured":"Bordini, R. H., Fisher, M., Pardavila, C., & Wooldridge, M. (2003). Model checking AgentSpeak. In J. S. Rosenschein, T. Sandholm, M. Wooldridge, & M. Yokoo (Eds.), Proceedings of the second international joint conference on autonomous agents and multi-agent systems (AAMAS-2003), Melbourne, Australia, 14\u201318 July, (pp. 409\u2013416) New York, NY, ACM Press.","DOI":"10.1145\/860575.860641"},{"issue":"5","key":"5955_CR5","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/MIS.2004.47","volume":"19","author":"R. H. Bordini","year":"2004a","journal-title":"IEEE Intelligent Systems"},{"key":"5955_CR6","unstructured":"Bordini, R. H., Fisher, M., Visser, W., & Wooldridge, M. (2004b) State-space reduction techniques in agent verification. In N. R. Jennings, C. Sierra, L. Sonenberg & M. Tambe (Eds.). Proceedings of the third international joint conference on autonomous agents and multi-agent systems (AAMAS-2004), New York, NY, 19\u201323 July (pp. 896\u2013903) New York, NY, ACM Press."},{"key":"5955_CR7","doi-asserted-by":"crossref","unstructured":"Bordini, R. H., Fisher, M., Visser W., & Wooldridge, M (2004c) Verifiable multi-agent programs. In M. Dastani, J. Dix, & A. El Fallah-Seghrouchni, (Eds.)Programming multi-agent systems, proceedings of the first international workshop (ProMAS-03), held with AAMAS-03, 15 July, 2003, Melbourne, Australia (Selected Revised and Invited Papers), number 3067 in Lecture notes in artificial intelligence, (pp. 72\u201389) Berlin, Springer-Verlag.","DOI":"10.1007\/978-3-540-25936-7_4"},{"key":"5955_CR8","unstructured":"Bordini, R. H., H\u00fcbner, J. F., et al. (2005) Jason. http:\/\/jason.sourceforge.net\/."},{"key":"5955_CR9","doi-asserted-by":"crossref","unstructured":"Bordini, R. H., H\u00fcbner, J. F., & Vieira, R. (2005). Jason and the golden fleece of agent-oriented programming. In R. H. Bordini, M. Dastani, J. Dix, & A. El Fallah Seghrouchni, (Eds.) Multi-agent programming: Languages, Platforms and applications, chap. 1 Springer-Verlag.","DOI":"10.1007\/0-387-26350-0_1"},{"key":"5955_CR10","doi-asserted-by":"crossref","unstructured":"Bordini, R. H., & Moreira, \u00c1. F. (2004 September). Proving BDI properties of agent-oriented programming languages: The asymmetry thesis principles in AgentSpeak(L). Annals of Mathematics and Artificial Intelligence, 42 (1\u20133), 197\u2013226. Special issue on computational logic in multi-agent systems.","DOI":"10.1023\/B:AMAI.0000034527.45635.e5"},{"key":"5955_CR11","doi-asserted-by":"crossref","unstructured":"Bordini R. H., Visser W., Fisher, M., Pardavila, C., & Wooldridge, M. (2003). Model checking multi-agent programs with CASP. In W.A. Hunt Jr. & F. Somenzi, (Eds.) Proceedgins of the fifteenth conference on computer-aided verification (CAV-2003), Boulder, CO, 8\u201312 July, number 2725 in Lecture Notes in Computer Science, (pp. 110\u2013113) Berlin: Springer-Verlag. Tool description.","DOI":"10.1007\/978-3-540-45069-6_10"},{"key":"5955_CR12","volume-title":"Model checking","author":"E. M. Clarke","year":"2000"},{"issue":"3","key":"5955_CR13","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0004-3702(90)90055-5","volume":"42","author":"P. R. Cohen","year":"1990","journal-title":"Artificial Intelligence"},{"key":"5955_CR14","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, S. L., & Zheng, H. (2000, June) Bandera : Extracting finite-state models from java source code. In Proceedings of the 22nd international conference on software engineering, Limeric, Ireland: ACM Press.","DOI":"10.1145\/337180.337234"},{"key":"5955_CR15","doi-asserted-by":"crossref","unstructured":"d\u2019Inverno, M., Kinny, D., Luck, M., & Wooldridge, M. (1998). A formal specification of dMARS. In M. P. Singh, A. S. Rao, & M. Wooldridge, (Eds.), Intelligent agents IV\u2014proceedings of the fourth international workshop on agent theories, architectures, and languages (ATAL-97), providence, RI, 24\u201326 July, 1997, number 1365 in Lecture notes in artificial intelligence, (pp. 155\u2013176). Berlin: Springer-Verlag.","DOI":"10.1007\/BFb0026757"},{"issue":"3","key":"5955_CR16","first-page":"1","volume":"8","author":"M. d\u2019Inverno","year":"1998","journal-title":"Journal of Logic and Computation"},{"key":"5955_CR17","doi-asserted-by":"crossref","unstructured":"Fisher, M. (2005, January) Temporal development methods for agent-Based systems. Journal of Autonomous Agents and Multi-Agent Systems, 10(1), 41\u201366.","DOI":"10.1007\/s10458-004-3140-4"},{"key":"5955_CR18","unstructured":"Fisher, M., & Visser, W. (2002). Verification of autonomous spacecraft control\u2014a logical vision of the future. In Proceedings of the workshop on AI planning and scheduling for autonomy in space applications, co-located with TIME-2002, 7\u20139 July, Manchester, UK."},{"key":"5955_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D. Harel","year":"2000"},{"key":"5955_CR20","doi-asserted-by":"crossref","unstructured":"Havelund, K., Lowry, M., & Penix, J. (2001, August). Formal analysis of a space craft controller using SPIN. IEEE Transactions on Software Engineering, 27(8).","DOI":"10.1109\/32.940728"},{"key":"5955_CR21","first-page":"95","volume-title":"Model checking software, proceedings of SPIN 2002 (LNCS Volume 2318)","author":"W. Hoek van der","year":"2002"},{"key":"5955_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann, G. (1997, May). The Spin model checker. IEEE Transaction on Software Engineering, 23(5), 279\u2013295","DOI":"10.1109\/32.588521"},{"key":"5955_CR23","unstructured":"Holzmann, G. J. (1991). Design and validation of computer protocols. Prentice Hall."},{"key":"5955_CR24","unstructured":"Java PathFinder. http:\/\/javapathfinder.sourceforge.net."},{"key":"5955_CR25","volume-title":"The distributed multi-agent reasoning system architecture and language specification","author":"D. Kinny","year":"1993"},{"key":"5955_CR26","doi-asserted-by":"crossref","unstructured":"Labrou, Y., & Finin, T. (1994, November). A semantics approach for KQML\u2014a general purpose communication language for software agents. In Proceedings of the third international conference on information and knowledge management (CIKM\u201994). ACM Press.","DOI":"10.1145\/191246.191320"},{"key":"5955_CR27","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0004-3702(98)00068-X","volume":"103","author":"N. Muscettola","year":"1998","journal-title":"Artificial Intelligence"},{"key":"5955_CR28","doi-asserted-by":"crossref","unstructured":"Muscettola, N., Nayak, P. P., Pell, B., & Williams, B. C. (1998b, August) Remote agent: To boldly go where no AI system has gone before. Artificial Intelligence, 103(1\u20132), 5\u201347.","DOI":"10.1016\/S0004-3702(98)00068-X"},{"key":"5955_CR29","volume-title":"A structural approach to operational semantics","author":"G. D. Plotkin","year":"1981"},{"key":"5955_CR30","doi-asserted-by":"crossref","unstructured":"Rao, A. S. (1996). AgentSpeak(L): BDI agents speak out in a logical computable language. In W. Van de Velde & J. Perram, (Eds.) Proceedings of the seventh workshop on modelling autonomous agents in a multi-agent world (MAAMAW\u201996) 22\u201325 January, Eindhoven, The Netherlands, number 1038 in Lecture notes in artificial intelligence (pp. 42\u201355) London. Springer-Verlag.","DOI":"10.1007\/BFb0031845"},{"key":"5955_CR31","unstructured":"Rao, A. S., & Georgeff, M. P. (1993) A model-theoretic approach to the verification of situated reasoning systems. In Proceedings of the thirteenth international joint conference on artificial intelligence (IJCAI-93) (pp. 318\u2013324) Chamb\u00e9ry, France."},{"issue":"3","key":"5955_CR32","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1093\/logcom\/8.3.293","volume":"8","author":"A. S. Rao","year":"1998","journal-title":"Journal of Logic and Computation"},{"key":"5955_CR33","doi-asserted-by":"crossref","unstructured":"Robby, M. Dwyer, B., & Hatcliff, J. (2003, March). Bogor: An extensible and highly-modular model checking framework. In In the proceedings of the fourth joint meeting of the european software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE).","DOI":"10.1145\/940071.940107"},{"key":"5955_CR34","unstructured":"Shoham, Y. (1990). Agent-oriented programming. Technical report STAN\u2013CS\u20131335\u201390, computer science department, Stanford University, Stanford, CA 94305."},{"key":"5955_CR35","first-page":"331","volume-title":"Multiagent systems\u2014a modern approach to distributed artificial intelligence","author":"M. P. Singh","year":"1999"},{"key":"5955_CR36","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., & Park, S. (2000). Model checking programs. In Proceedings of the fifteenth international conference on automated software engineering (ASE\u201900), 11\u201315 September, Grenoble, France (pp. 3\u201312) IEEE Computer Society.","DOI":"10.1109\/ASE.2000.873645"},{"key":"5955_CR37","doi-asserted-by":"crossref","unstructured":"Washington, R., Golden, K., Bresina, J., Smith, D. E., Anderson, C., & Smith, T. (1999). Autonomous rovers for mars exploration. In Aerospace conference, 6\u201313 March, Aspen, CO, Vol. 1 (pp. 237\u2013251) IEEE.","DOI":"10.1109\/AERO.1999.794236"},{"key":"5955_CR38","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about rational agents","author":"M. Wooldridge","year":"2000"},{"key":"5955_CR39","first-page":"952","volume-title":"Proceedings of the first international joint conference on autonomous agents and multi-agent systems (AAMAS-2002), 15\u201319 July, Bologna, Italy","author":"M. Wooldridge","year":"2002"}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-006-5955-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10458-006-5955-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-006-5955-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T21:26:28Z","timestamp":1736285188000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10458-006-5955-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2,24]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["5955"],"URL":"https:\/\/doi.org\/10.1007\/s10458-006-5955-7","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"value":"1387-2532","type":"print"},{"value":"1573-7454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2,24]]}}}