Skip to main content
SpringerLink
Log in

A Verification Logic for Goal Agents

  • Chapter
  • First Online:
Specification and Verification of Multi-agent Systems

Abstract

Although there has been a growing body of literature on verification of agents programs, it has been difficult to design a verification logic for agent programs that fully characterizes such programs and to connect agent programs to agent theory. The challenge is to define an agent programming language that defines a computational framework but also allows for a logical characterization useful for verification. The agent programming language Goal has been originally designed to connect agent programming to agent theory and we present additional results here that Goal agents can be fully represented by a logical theory. Goal agents can thus be said to execute the corresponding logical theory.

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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. Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Directions for agent model checking. In: this volume, Chapter 4

    Google Scholar 

  2. Hindriks, K., de Boer, F., van der Hoek, W., Meyer, J.-J. Ch.: A Programming Logic for part of the Agent Language 3APL . In: J. Rash (ed.) Proceedings of the First Goddard Workshop on Formal Approaches to Agent-Based Systems , pp. 78–89. Springer-Verlag (2001)

    Google Scholar 

  3. Reiter, R.: The Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression . In: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 359–380. Academic Press (1991)

    Google Scholar 

  4. Alechina, N., Dastani, M., Logan, B., Meyer, J.-J. Ch.: Reasoning about agent deliberation. In: G. Brewka, J. Lang (eds.) Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning (KR’08), pp. 16–26. AAAI, Sydney, Australia (2008)

    Google Scholar 

  5. Liu, Y.: A Hoare-style proof system for robot programs . In: Proceedings of the Eighteenth National Conference on Artificial intelligence (AAAI/IAAI’02), pp. 74 – 79 (2002)

    Google Scholar 

  6. Dastani, M., van Riemsdijk, M.B., Meyer, J.-J. Ch.: Goal types in agent programming. In: Proceedings of the 17th European Conference on Artifical Intelligence 2006 (ECAI’06), Frontiers in Artificial Intelligence and Applications, vol. 141, pp. 220–224. IOS Press (2006)

    Google Scholar 

  7. Hindriks, K., van der Hoek, W.: Goal agents instantiate intention logic. In: Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA’08), pp. 232–244 (2008)

    Google Scholar 

  8. Meyer, J.-J. Ch., van der Hoek, W.: Epistemic Logic for AI and Computer Science. Cambridge: Cambridge University Press (1995)

    Book  MATH  Google Scholar 

  9. Lloyd, J.W.: Foundations of Logic Programming. Springer-Verlag (1993)

    Google Scholar 

  10. Giacomo, G.d., Lespérance, Y., Levesque, H.: ConGolog, a Concurrent Programming Language Based on the Situation Calculus . Artificial Intelligence 121(1-2), 109–169 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  11. Apt, K.R., Bol, R.: Logic programming and negation: A survey. Journal of Logic Programming 19, 9–71 (1994)

    Article  MathSciNet  Google Scholar 

  12. Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice . Morgan Kaufmann (2004)

    Google Scholar 

  13. Hindriks, K.V., van Riemsdijk, M.B., van der Hoek, W.: Agent programming with temporally extended goals. In: Proceedings of the 8th International Conference on Autonomous Agents and Multi-Agent Systems, p. to appear (2009)

    Google Scholar 

  14. Bacmair, L., Ganzinger, H.: Resolution theorem proving. In: J.A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, chap. 2, pp. 19–99. Elsevier and MIT Press (2001)

    Google Scholar 

  15. Pednault, E.P.: ADL and the State-Transition Model of Action . Journal of Logic and Computation 4(5), 467–512 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  16. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer-Verlag (1995)

    Google Scholar 

  17. Duff, S., Harland, J., Thangarajah, J.: On Proactivity and Maintenance Goals . In: Proceedings of the fifth international joint conference on autonomous agents and multiagent systems (AAMAS’06), pp. 1033–1040. Hakodate (2006)

    Google Scholar 

  18. Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York, NY, USA (1992)

    Google Scholar 

  19. Hindriks, K.V.: Programming Rational Agents in GOAL . In: Bordini et al. [65], chap. 4, pp. 119–157

    Google Scholar 

  20. de Boer, F.S., Hindriks, K.V., van der Hoek , W., Meyer, J.-J. Ch.: A Verification Framework for Agent Programming with Declarative Goals. Journal of Applied Logic 5(2), 277–302 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  21. Shapiro, S., Lespérance, Y., Levesque, H.J.: The cognitive agents specification language and verification environment for multiagent systems. In: Proceedings of the first international joint conference on autonomous agents and multiagent systems (AAMAS’02), pp. 19–26 (2002)

    Google Scholar 

  22. Hindriks, K.V., Roberti, T.: Goal as a planning formalism. In: Proceedings of MATES 2009 (2009)

    Google Scholar 

  23. Mayer, M.C., Limongelli, C., Orlandini, A., Poggioni, V.: Linear temporal logic as an executable semantics for planning languages . Journal of Logic, Lang and Information 16, 63–89 (2007)

    Article  MATH  Google Scholar 

  24. Hindriks, K.: Modules as Policy-Based Intentions: Modular Agent Programming in GOAL . In: Proceedings of the International Workshop on Programming Multi-Agent Systems (ProMAS’07), vol. 4908, pp. 156–171 (2008)

    Google Scholar 

  25. Newell, A.: The Knowledge Level . Artificial Intelligence 18(1), 87–127 (1982)

    Article  Google Scholar 

  26. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)

    Google Scholar 

  27. Hindriks, K.V., Lespérance, Y., Levesque, H.: An Embedding of ConGolog in 3APL . In: Proceedings of the 14th European Conference on Artificial Intelligence (ECAI’00), pp. 558–562 (2000)

    Google Scholar 

  28. Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J. Ch.: Agent Programming in 3APL . Autonomous Agents and Multi-Agent Systems 2(4), 357–401 (1999)

    Article  Google Scholar 

  29. de Bakker, J.: Mathematical Theory of Program Correctness. Prentice Hall, Inc. (1980)

    Google Scholar 

  30. Shapiro, S., Lespérance, Y., Levesque, H.J.: Goal change in the situation calculus. Journal of Logic and Computation 17(5), 983–1018 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  31. Hindriks, K., van Riemsdijk, B.: A computational semantics for communicating rational agents based on mental models. In: Proceedings of the International Workshop on Programming Multi-Agent Systems (ProMAS’09) (to appear)

    Google Scholar 

  32. Plotkin, G.D.: A Structural Approach to Operational Semantics . Tech. Rep. DAIMI FN-19, University of Aarhus (1981)

    Google Scholar 

  33. Thiébaux, S., Hoffmann, J., Nebel, B.: In defense of PDDL axioms . Artificial Intelligence 168, 38–69 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  34. Dastani, M.: 2APL : A practical agent programming language. Autonomous Agents and Multi-Agent Systems 16(3), 214–248 (2008)

    Article  Google Scholar 

Download references

Acknowledgements

The work presented would not have been possible without many useful discussions and comments from, in particular, Frank de Boer, Wiebe van der Hoek, and John-Jules Ch. Meyer. I’d like to thank them here for the interesting exchanges on the topic of verification.

Author information

Authors and Affiliations

  1. Delft University of Technology, Delft, The Netherlands

    K.V. Hindriks

Authors
  1. K.V. Hindriks
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to K.V. Hindriks .

Editor information

Editors and Affiliations

  1. Dept. Information & Computing Sciences, Utrecht University, Padualaan 14, Utrecht, 3584 CH, Netherlands

    Mehdi Dastani

  2. Delft University of Technology, Mekelweg 4, Delft, 2628 CD, Netherlands

    Koen V. Hindriks

  3. Dept. Information & Computer Sciences, Utrecht University, Utrecht, Netherlands

    John-Jules Charles Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer Science+Business Media, LLC

About this chapter

Cite this chapter

Hindriks, K. (2010). A Verification Logic for Goal Agents. In: Dastani, M., Hindriks, K., Meyer, JJ. (eds) Specification and Verification of Multi-agent Systems. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-6984-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-1-4419-6984-2_8

  • Published:

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4419-6983-5

  • Online ISBN: 978-1-4419-6984-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation