Skip to main content
SpringerLink
Log in

Our Quest for the Holy Grail of Agent Verification

  • Conference paper
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4548))

Abstract

Since the inception of agent technology almost two decades ago, researchers have worked both on the formal, theoretical aspects of intelligent agents and on the realisation / implementation of them. However, the link between the two has always remained rather unclear, to this day. Although there is a definite need for the verification of agents, the methods and techniques for this are still in their infancy. We describe our personal ongoing quest for the ‘right’ approach to agent verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aldewereld, H.: Autonomy vs. Conformity: An Institutional Perspective on Norms and Ptotocols, Ph.D. thesis, Utrecht University, Utrecht (2007)

    Google Scholar 

  2. Aldewereld, H., Dignum, F., Meyer, J.-J.Ch.: Designimg Protocols for Agent Institutions, accepted for ProMAS 2007 (2007)

    Google Scholar 

  3. Aldewereld, H., Vázquez-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ázquez-Salceda, J. (eds.) Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems. LNCS (LNAI), vol. 3913, pp. 231–245. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Alechina, N., Dastani, M., Logan, B., Meyer, J.-J.Ch.: A Logic of Agent Programs. In: Proc. AAAI-07 (to appear, 2007)

    Google Scholar 

  5. Audi, R. (ed.): The Cambridge Dictionary of Philosophy. Cambridge Univ. Press, Cambridge (1999)

    Google Scholar 

  6. de Bakker, J.W.: Mathematical Theory of Program Correctness. Prentice-Hall International, London (1980)

    MATH  Google Scholar 

  7. Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming. Kluwer, Boston, Dordrecht, London (2005)

    MATH  Google Scholar 

  8. 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)

    Google Scholar 

  9. 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)

    Article  Google Scholar 

  10. Bratman, M.E.: Intentions, Plans, and Practical Reason. Harvard University Press, Massachusetts (1987)

    Google Scholar 

  11. Chandy, K.M., Misra, J.: Parallel Program Design. Addison-Wesley, London (1988)

    MATH  Google Scholar 

  12. Cohen, P.R., Levesque, H.J.: Intention is Choice with Commitment. Artificial Intelligence 42(3), 213–261 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  13. Dastani, M., Meyer, J.-J.Ch.: A Practical Agent Programming Language, accepted for ProMAS 2007 (2007)

    Google Scholar 

  14. 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. 3067, Springer, Heidelberg (2004)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. Dennett, D.: The Intentional Stance, Bradford Books/MIT Press, Cambridge MA (1987)

    Google Scholar 

  17. Dignum, V.: A Model for Organizational Interaction (Based on Agents, Founded in Logic), Ph.D. Thesis, Utrecht University, Utrecht (2004)

    Google Scholar 

  18. Emerson, E.A., Halpern, J.Y.: Sometimes and Not Never Revisited: on Branching versus Linear Time Temporal Logic. J. ACM 33(1), 151–178 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  19. 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. 2333, pp. 348–366. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Fischer, M.J., Ladner, R.E.: Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci 18(2), 194–211 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  21. Fisher, M.: A Survey of Concurrent METATEM – The language and Its Applications. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol. 827, pp. 480–505. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  22. 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. 3900, pp. 129–142. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Hindriks, K.V.: Agent Programming Languages: Programming with Mental Models, Ph.D. thesis, Utrecht University, Utrecht (2001)

    Google Scholar 

  24. 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 2(4), 357–401 (1999)

    Article  Google Scholar 

  25. Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J.Ch.: Agent Programming with Declarative Goals. In: Castelfranchi, C., Lespérance, Y. (eds.) ATAL 2000. LNCS (LNAI), vol. 1986, pp. 228–243. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. 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–15 (2006)

    Google Scholar 

  27. 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. 4314, pp. 404–418. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  28. 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. 14, pp. 133–168. Kluwer, Dordrecht (1998)

    Google Scholar 

  29. 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–213. IEEE Press, Los Alamitos, CA, USA (2001)

    Google Scholar 

  30. 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–225. Springer, Berlin (2006)

    Google Scholar 

  31. 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. 3920, pp. 450–454. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  32. 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 9(2), 245–256 (2001)

    Article  MATH  Google Scholar 

  33. Ölveczky, P.C.: Formal Modeling and Analysis of Distributed Systems in Maude, lecture notes (2005)

    Google Scholar 

  34. 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. 1038, pp. 42–55. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  35. 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–484. Morgan Kaufmann, Washington (1991)

    Google Scholar 

  36. Rash, J.L., Rouff, C.A., Truszkowski, W., Gordon, D.F., Hinchey, M.G. (eds.): FAABS 2000. LNCS (LNAI), vol. 1871. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  37. van Riemsdijk, M.B.: Cognitive Agent Programming: A Semantic Approach, Ph.D. Thesis, Utrecht University, Utrecht (2006)

    Google Scholar 

  38. 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–400. ACM Press, New York (2003)

    Google Scholar 

  39. 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. 4371, pp. 95–114. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  40. van Riemsdijk, M.B., de Boer, F.S., Meyer, J.-J.: Dynamic Logic for Plan Revision in Intelligent Agents. J Logic Computation 16(3), 375–402 (2006)

    Article  MATH  Google Scholar 

  41. Schmidt, R.A.: PDL-TABLEAU (2003), http://www.cs.man.ac.uk/schmidt/pdl-tableau

  42. Shoham, Y.: Agent-Oriented Programming. Artificial Intelligence 60(1), 51–92 (1993)

    Article  MathSciNet  Google Scholar 

  43. Wooldridge, M.J.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  44. van der Hoek, W., Wooldridge, M.: Towards a Logic of Rational Agency. Logic Journal of the IGPL 11(2), 133–157 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information and Computing Sciences, Utrecht University, The Netherlands

    John-Jules Ch. Meyer

Authors
  1. John-Jules Ch. Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Nicola Olivetti

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Meyer, JJ.C. (2007). Our Quest for the Holy Grail of Agent Verification. In: Olivetti, N. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2007. Lecture Notes in Computer Science(), vol 4548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73099-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73099-6_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73098-9

  • Online ISBN: 978-3-540-73099-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation