Skip to main content
SpringerLink
Log in

Using Theorem Proving to Verify Properties of Agent Programs

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

Abstract

We present a sound and complete logic for automatic verification of simpleAPL programs. simpleAPL is a simplified version of agent programming languages such as 3APL and 2APL designed for the implementation of cognitive agents with beliefs, goals and plans. Our logic is a variant of PDL, and allows the specification of safety and liveness properties of agent programs. We prove a correspondence between the operational semantics of simpleAPL and the models of the logic for two example program execution strategies. We show how to translate agent programs written in simpleAPL into expressions of the logic, and give an example in which we show how to verify correctness properties for a simple agent program using theorem-proving.

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

  3. Scherl, R.B., Levesque, H.J.: Knowledge, action, and the frame problem. Artificial Intelligence 144(1–2), 1–39 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  4. van Riemsdijk, M., de Boer, F., Dastani, M., Meyer, J.-J. Ch.: Prototyping 3apl in the maude term rewriting language. In: Proceedings of the seventh International Workshop on Computational Logic in Multi-Agent Systems (CLIMA 2006), LNAI, vol. 4371. Springer (2007)

    Google Scholar 

  5. van Ditmarsch, H.P., Herzig, A., De Lima, T.: Optimal regression for reasoning about knowledge and actions. In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence (AAAI 2007), pp. 1070–1075. AAAI Press (2007)

    Google Scholar 

  6. Fisher, M.: MetateM: The Story so Far. In: Proc. 3rd International Workshop on Programming Multiagent Systems (ProMAS), LNAI, vol. 3862, pp. 3–22. Springer Verlag (2006)

    Google Scholar 

  7. Dastani, M., Meyer, J.-J. Ch.: Correctness of multi-agent programs: A hybrid approach. In: this volume, Chapter 6

    Google Scholar 

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

  9. van Riemsdijk, M.B., Astefanoaei, L., de Boer, F.S.: Using the Maude term rewriting language for agent development with formal foundations. In: this volume, Chapter 11

    Google Scholar 

  10. Hustadt, U., Schmidt, R.A.: MSPASS : Modal reasoning by translation and first-order resolution. In: Proc. TABLEAUX 2000, LNCS, vol. 1847, pp. 67–71. Springer (2000)

    Google Scholar 

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

  12. Astefanoaei, L., Dastani, M., de Boer, F., Meyer, J.-J. Ch.: A verification framework for normative multi-agent systems. In: In the proceedings of The 11th Pacific Rim International Conference on Multi-Agents (PRIMA 2008), LNAI, vol. 5357. Springer (2008)

    Google Scholar 

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

    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: Proc. ProMAS 2003, LNCS, vol. 3067, pp. 111–130. Springer (2004)

    Google Scholar 

  15. Dastani, M., Meyer, J.-J. Ch.: A practical agent programming language. In: M. Dastani, A.E. Fallah-Seghrouchni, A. Ricci, M. Winikoff (eds.) Proceedings of the Fifth International Workshop on Programming Multi-agent Systems ( ProMAS ’07), LNCS, vol. 4908, pp. 107–123. Springer (2008)

    Google Scholar 

  16. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)

    Google Scholar 

  17. Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming: Languages, Platforms and Applications. Springer-Verlag (2005)

    Google Scholar 

  18. Alechina, N., Dastani, M., Logan, B., Meyer, J.-J. Ch.: A logic of agent programs. In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence (AAAI 2007), pp. 795–800. AAAI Press (2007)

    Google Scholar 

  19. Bordini, R.H., Hübner, J.F., Vieira, R.: 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 (2005)

    Google Scholar 

  20. Hindriks, K., Meyer, J.-J. Ch.: Agent logics as program logics: Grounding KARO . In: Proc. 29th German Conference on AI (KI 2006), LNAI, vol. 4314. Springer (2007)

    Google Scholar 

  21. 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 

  22. Lomuscio, A., Raimondi, F.: Mcmas: A model checker for multi-agent systems. In: Proc. TACAS 2006 , pp. 450–454 (2006)

    Google Scholar 

  23. 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 

  24. Abrahamson, K.R.: Decidability and expressiveness of logics of processes. Ph.D. thesis, Department of Computer Science, University of Washington (1980)

    Google Scholar 

  25. Dastani, M., van Riemsdijk, M.B., Meyer, J.-J. Ch.: A grounded specification language for agent programs. In: Proceedings of the Sixth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’07), pp. 578–585. IFAAMAS, Honolulu, Hawaii (2007)

    Google Scholar 

  26. Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: W.V. de Velde, J. Perrame (eds.) Agents Breaking Away: Proceedings of the Seventh European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW’96), pp. 42–55. Springer Verlag, LNAI 1038 (1996)

    Google Scholar 

  27. Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying Multi-Agent Programs by Model Checking . Journal of Autonomous Agents and Multi-Agent Systems 12(2), 239–256 (2006)

    Article  Google Scholar 

  28. Shapiro, S., Lesperance, Y., Levesque, H.: The cognitive agent specification language and verification environment. In: this volume, Chapter 9

    Google Scholar 

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

    Article  Google Scholar 

  30. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press: Cambridge, MA (1995)

    MATH  Google Scholar 

  31. Benerecetti, M., Giunchiglia, F., Serafini, L.: Model checking multiagent systems. Journal of Logic and Computation 8(3), 401–423 (1998)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Acknowledgements

We would like to thank to Renate Schmidt for help with MSPASS and PDL-TABLEAU. Natasha Alechina and Brian Logan were supported by the Engineering and Physical Sciences Research Council [grant number EP/E031226].

Author information

Authors and Affiliations

  1. University of Nottingham, School of Computer Science, Nottingham, UK

    N. Alechina, F. Khan & B. Logan

  2. Department of Information and Computing Sciences, Universiteit Utrecht, Utrecht, The Netherlands

    M. Dastani & J.-J. Ch. Meyer

Authors
  1. N. Alechina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. Dastani
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. F. Khan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. B. Logan
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. J.-J. Ch. Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to N. Alechina .

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

Alechina, N., Dastani, M., Khan, F., Logan, B., Meyer, JJ.C. (2010). Using Theorem Proving to Verify Properties of Agent Programs. 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_1

Download citation

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

  • 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