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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Directions for agent model checking. In: this volume, Chapter 4
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)
Scherl, R.B., Levesque, H.J.: Knowledge, action, and the frame problem. Artificial Intelligence 144(1–2), 1–39 (2003)
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)
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)
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)
Dastani, M., Meyer, J.-J. Ch.: Correctness of multi-agent programs: A hybrid approach. In: this volume, Chapter 6
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)
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
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)
Schmidt, R.A.: pdl-tableau (2003). http://www.cs.man.ac.uk/schmidt/pdl-tableau
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)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
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)
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)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)
Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming: Languages, Platforms and Applications. Springer-Verlag (2005)
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)
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)
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)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)
Lomuscio, A., Raimondi, F.: Mcmas: A model checker for multi-agent systems. In: Proc. TACAS 2006 , pp. 450–454 (2006)
van der Hoek, W., Wooldridge, M.: Towards a logic of rational agency. Logic Journal of the IGPL 11(2), 133–157 (2003)
Abrahamson, K.R.: Decidability and expressiveness of logics of processes. Ph.D. thesis, Department of Computer Science, University of Washington (1980)
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)
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)
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)
Shapiro, S., Lesperance, Y., Levesque, H.: The cognitive agent specification language and verification environment. In: this volume, Chapter 9
Dastani, M.: 2APL : A practical agent programming language. Autonomous Agents and Multi-Agent Systems 16(3), 214–248 (2008)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press: Cambridge, MA (1995)
Benerecetti, M., Giunchiglia, F., Serafini, L.: Model checking multiagent systems. Journal of Logic and Computation 8(3), 401–423 (1998)
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)