{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:28:19Z","timestamp":1737437299216,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73099-6_2","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"2-9","source":"Crossref","is-referenced-by-count":3,"title":["Our Quest for the Holy Grail of Agent Verification"],"prefix":"10.1007","author":[{"given":"John-Jules Ch.","family":"Meyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Aldewereld, H.: Autonomy vs. Conformity: An Institutional Perspective on Norms and Ptotocols, Ph.D. thesis, Utrecht University, Utrecht (2007)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Aldewereld, H., Dignum, F., Meyer, J.-J.Ch.: Designimg Protocols for Agent Institutions, accepted for ProMAS 2007 (2007)","DOI":"10.1145\/1329125.1329163"},{"key":"2_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/11775331_16","volume-title":"Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems","author":"H. Aldewereld","year":"2006","unstructured":"Aldewereld, H., V\u00e1zquez-Salceda, J., Dignum, F., Meyer, J.-J.Ch.: Verifying Norm Compliancy of Protocols. In: Boissier, O., Padget, J., Dignum, V., Lindemann, G., Matson, E., Ossowski, S., Sichman, J.S., V\u00e1zquez-Salceda, J. (eds.) Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems. LNCS (LNAI), vol.\u00a03913, pp. 231\u2013245. Springer, Heidelberg (2006)"},{"key":"2_CR4","unstructured":"Alechina, N., Dastani, M., Logan, B., Meyer, J.-J.Ch.: A Logic of Agent Programs. In: Proc. AAAI-07 (to appear, 2007)"},{"volume-title":"The Cambridge Dictionary of Philosophy","year":"1999","key":"2_CR5","unstructured":"Audi, R. (ed.): The Cambridge Dictionary of Philosophy. Cambridge Univ. Press, Cambridge (1999)"},{"key":"2_CR6","volume-title":"Mathematical Theory of Program Correctness","author":"J.W. Bakker de","year":"1980","unstructured":"de Bakker, J.W.: Mathematical Theory of Program Correctness. Prentice-Hall International, London (1980)"},{"volume-title":"Multi-Agent Programming","year":"2005","key":"2_CR7","unstructured":"Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming. Kluwer, Boston, Dordrecht, London (2005)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Bordini, R.H., Moreira, A.F.: Proving the Asymmetry Thesis Principles for a BDI Agent-Oriented Programming Language, Electronic Notes in Theoretical Computer Science 70(5) (2002)","DOI":"10.1016\/S1571-0661(04)80591-7"},{"issue":"2","key":"2_CR9","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"R.H. Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. Autonomous Agents and Multi-Agent Systems\u00a012(2), 239\u2013256 (2006)","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"2_CR10","volume-title":"Intentions, Plans, and Practical Reason","author":"M.E. Bratman","year":"1987","unstructured":"Bratman, M.E.: Intentions, Plans, and Practical Reason. Harvard University Press, Massachusetts (1987)"},{"key":"2_CR11","volume-title":"Parallel Program Design","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design. Addison-Wesley, London (1988)"},{"issue":"3","key":"2_CR12","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0004-3702(90)90055-5","volume":"42","author":"P.R. Cohen","year":"1990","unstructured":"Cohen, P.R., Levesque, H.J.: Intention is Choice with Commitment. Artificial Intelligence\u00a042(3), 213\u2013261 (1990)","journal-title":"Artificial Intelligence"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Dastani, M., Meyer, J.-J.Ch.: A Practical Agent Programming Language, accepted for ProMAS 2007 (2007)","DOI":"10.1145\/1329125.1329294"},{"key":"2_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","DOI":"10.1007\/b98149","volume-title":"Programming Multi-Agent Systems","author":"M. Dastani","year":"2004","unstructured":"Dastani, M., van Riemsdijk, M.B., Dignum, F., Meyer, J.-J.Ch.: A Programming Language for Cognitive Agents: Goal-Directed 3APL. In: Dastani, M., Dix, J., El Fallah-Seghrouchni, A. (eds.) PROMAS 2003. LNCS (LNAI), vol.\u00a03067, Springer, Heidelberg (2004)"},{"key":"2_CR15","volume-title":"Proc. AAMAS 2007","author":"M. Dastani","year":"2007","unstructured":"Dastani, M., van Riemsdijk, B., Meyer, J.-J.Ch.: A Grounded Specification Language for Agent Programs. In: Proc. AAMAS 2007, ACM Press, New York (2007)"},{"key":"2_CR16","unstructured":"Dennett, D.: The Intentional Stance, Bradford Books\/MIT Press, Cambridge MA (1987)"},{"key":"2_CR17","unstructured":"Dignum, V.: A Model for Organizational Interaction (Based on Agents, Founded in Logic), Ph.D. Thesis, Utrecht University, Utrecht (2004)"},{"issue":"1","key":"2_CR18","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and Not Never Revisited: on Branching versus Linear Time Temporal Logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"2_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-45448-9_26","volume-title":"Intelligent Agents VIII","author":"M. Esteva","year":"2002","unstructured":"Esteva, M., Padget, J., Sierra, C.: Formalizing a Language for Institutions and Norms. In: Meyer, J.-J.Ch., Tambe, M. (eds.) ATAL 2001. LNCS (LNAI), vol.\u00a02333, pp. 348\u2013366. Springer, Heidelberg (2002)"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci\u00a018(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/BFb0014005","volume-title":"Temporal Logic","author":"M. Fisher","year":"1994","unstructured":"Fisher, M.: A Survey of Concurrent METATEM \u2013 The language and Its Applications. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol.\u00a0827, pp. 480\u2013505. Springer, Heidelberg (1994)"},{"key":"2_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/11750734_8","volume-title":"Computational Logic in Multi-Agent Systems","author":"M. Fisher","year":"2006","unstructured":"Fisher, M.: Implementing Temporal Logics: Tools for Execution and Proof (Tutorial Paper). In: Toni, F., Torroni, P. (eds.) Computational Logic in Multi-Agent Systems. LNCS (LNAI), vol.\u00a03900, pp. 129\u2013142. Springer, Heidelberg (2006)"},{"key":"2_CR23","unstructured":"Hindriks, K.V.: Agent Programming Languages: Programming with Mental Models, Ph.D. thesis, Utrecht University, Utrecht (2001)"},{"issue":"4","key":"2_CR24","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1023\/A:1010084620690","volume":"2","author":"K.V. Hindriks","year":"1999","unstructured":"Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J.Ch.: Agent Programming in 3APL. Int. J. of Autonomous Agents and Multi-Agent Systems\u00a02(4), 357\u2013401 (1999)","journal-title":"Int. J. of Autonomous Agents and Multi-Agent Systems"},{"key":"2_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/3-540-44631-1_16","volume-title":"Intelligent Agents VII. Agent Theories Architectures and Languages","author":"K.V. Hindriks","year":"2001","unstructured":"Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J.Ch.: Agent Programming with Declarative Goals. In: Castelfranchi, C., Lesp\u00e9rance, Y. (eds.) ATAL 2000. LNCS (LNAI), vol.\u00a01986, pp. 228\u2013243. Springer, Heidelberg (2001)"},{"key":"2_CR26","unstructured":"Hindriks, K.V., Meyer, J.-J.Ch.: An Agent Program Logic with Declarative Goals. In: Dunin-Keplicz, B., Verbrugge, R. (eds.) Proc. FAMAS 2006 (ECAI, Workshop on Formal Aspects of Multi-Agent Systems) ECCAI, pp. 1\u201315 (2006)"},{"key":"2_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-69912-5_30","volume-title":"KI 2006: Advances in Artificial Intelligence","author":"K.V. Hindriks","year":"2007","unstructured":"Hindriks, K.V., Meyer, J.-J.Ch.: Agent Logics as Program Logics: Grounding KARO. In: Freksa, C., Kohlhase, M., Schill, K. (eds.) KI 2006. LNCS (LNAI), vol.\u00a04314, pp. 404\u2013418. Springer, Heidelberg (2007)"},{"key":"2_CR28","first-page":"133","volume-title":"Foundations of Rational Agency. Applied Logic Series","author":"W. Hoek van der","year":"1998","unstructured":"van der Hoek, W., van Linder, B., Meyer, J.-J.Ch.: An Integrated Modal Approach to Rational Agents. In: Wooldridge, M., Rao, A. (eds.) Foundations of Rational Agency. Applied Logic Series, vol.\u00a014, pp. 133\u2013168. Kluwer, Dordrecht (1998)"},{"key":"2_CR29","first-page":"206","volume-title":"Cividale del Friuli, Italy. Eighth International Symposium (TIME-01)","author":"U. Hustadt","year":"2001","unstructured":"Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M., Meyer, J.-J.Ch.: Reasoning about Agents in the KARO Framework. In: Bettini, C., Montanari, A. (eds.) Cividale del Friuli, Italy. Eighth International Symposium (TIME-01), Cividale del Friuli, Italy, pp. 206\u2013213. IEEE Press, Los Alamitos, CA, USA (2001)"},{"key":"2_CR30","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/1-84628-271-3_7","volume-title":"Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering Series","author":"U. Hustadt","year":"2006","unstructured":"Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M., Meyer, J.-J.: Verification within the KARO Agent Theory. In: Rouff, C., Hinchey, M., Rash, J., Truszkowski, W., Gordon-Spears, D. (eds.) Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering Series, pp. 193\u2013225. Springer, Berlin (2006)"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/11691372_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: Mcmas: A Model Checker for Multi-Agent Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 450\u2013454. Springer, Heidelberg (2006)"},{"issue":"2","key":"2_CR32","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1093\/jigpal\/9.2.245","volume":"9","author":"J.-J. Meyer","year":"2001","unstructured":"Meyer, J.-J.Ch., de Boer, F.S., van Eijk, R.M., Hindriks, K.V., van der Hoek, W.: On Programming KARO Agents. Logic Journal of the IGPL\u00a09(2), 245\u2013256 (2001)","journal-title":"Logic Journal of the IGPL"},{"key":"2_CR33","unstructured":"\u00d6lveczky, P.C.: Formal Modeling and Analysis of Distributed Systems in Maude, lecture notes (2005)"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/BFb0031845","volume-title":"Agents Breaking Away","author":"A.S. Rao","year":"1996","unstructured":"Rao, A.S.: AgentSpeak(L): BDI Agents Speak Out in a Logical Computable Language. In: Perram, J., Van de Velde, W. (eds.) MAAMAW 1996. LNCS, vol.\u00a01038, pp. 42\u201355. Springer, Heidelberg (1996)"},{"key":"2_CR35","first-page":"473","volume-title":"Principles of Knowledge Representation and Reasoning","author":"A.S. Rao","year":"1991","unstructured":"Rao, A.S., Georgeff, M.P.: Modeling Rational Agents within a BDI-Architecture. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Principles of Knowledge Representation and Reasoning, pp. 473\u2013484. Morgan Kaufmann, Washington (1991)"},{"key":"2_CR36","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Formal Approaches to Agent-Based Systems","year":"2001","unstructured":"Rash, J.L., Rouff, C.A., Truszkowski, W., Gordon, D.F., Hinchey, M.G. (eds.): FAABS 2000. LNCS (LNAI), vol.\u00a01871. Springer, Heidelberg (2001)"},{"key":"2_CR37","unstructured":"van Riemsdijk, M.B.: Cognitive Agent Programming: A Semantic Approach, Ph.D. Thesis, Utrecht University, Utrecht (2006)"},{"key":"2_CR38","first-page":"393","volume-title":"Autonomous Agents and Multiagent Systems","author":"M.B. Riemsdijk van","year":"2003","unstructured":"van Riemsdijk, M.B., van der Hoek, W., Meyer, J.-J.: Agent Programming in Dribble: from Beliefs to Goals Using Plans. In: Rosenschein, J.S., Sandholm, T., Wooldridge, M., Yokoo, M. (eds.) Autonomous Agents and Multiagent Systems. 2nd Int. J. Conf (AAMASO03), Melbourne Australia, pp. 393\u2013400. ACM Press, New York (2003)"},{"key":"2_CR39","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-69619-3_6","volume-title":"Computational Logic in Multi-Agent Systems","author":"M.B. Riemsdijk van","year":"2007","unstructured":"van Riemsdijk, M.B., de Boer, F.S., Dastani, M., Meyer, J.-J.Ch.: Prototyping 3APL in the Maude Term Rewriting Language. In: Inoue, K., Satoh, K., Toni, F. (eds.) Computational Logic in Multi-Agent Systems. LNCS (LNAI), vol.\u00a04371, pp. 95\u2013114. Springer, Heidelberg (2007)"},{"issue":"3","key":"2_CR40","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1093\/logcom\/exi084","volume":"16","author":"M.B. Riemsdijk van","year":"2006","unstructured":"van Riemsdijk, M.B., de Boer, F.S., Meyer, J.-J.: Dynamic Logic for Plan Revision in Intelligent Agents. J Logic Computation\u00a016(3), 375\u2013402 (2006)","journal-title":"J Logic Computation"},{"key":"2_CR41","unstructured":"Schmidt, R.A.: PDL-TABLEAU (2003), http:\/\/www.cs.man.ac.uk\/schmidt\/pdl-tableau"},{"issue":"1","key":"2_CR42","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0004-3702(93)90034-9","volume":"60","author":"Y. Shoham","year":"1993","unstructured":"Shoham, Y.: Agent-Oriented Programming. Artificial Intelligence\u00a060(1), 51\u201392 (1993)","journal-title":"Artificial Intelligence"},{"key":"2_CR43","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about Rational Agents","author":"M.J. Wooldridge","year":"2000","unstructured":"Wooldridge, M.J.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)"},{"issue":"2","key":"2_CR44","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1093\/jigpal\/11.2.133","volume":"11","author":"W. Hoek van der","year":"2003","unstructured":"van der Hoek, W., Wooldridge, M.: Towards a Logic of Rational Agency. Logic Journal of the IGPL\u00a011(2), 133\u2013157 (2003)","journal-title":"Logic Journal of the IGPL"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T00:02:44Z","timestamp":1737417764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730989","9783540730996"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}