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.
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
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)
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)
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)
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)
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)
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)
Meyer, J.-J. Ch., van der Hoek, W.: Epistemic Logic for AI and Computer Science. Cambridge: Cambridge University Press (1995)
Lloyd, J.W.: Foundations of Logic Programming. Springer-Verlag (1993)
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)
Apt, K.R., Bol, R.: Logic programming and negation: A survey. Journal of Logic Programming 19, 9–71 (1994)
Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice . Morgan Kaufmann (2004)
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)
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)
Pednault, E.P.: ADL and the State-Transition Model of Action . Journal of Logic and Computation 4(5), 467–512 (1994)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer-Verlag (1995)
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)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York, NY, USA (1992)
Hindriks, K.V.: Programming Rational Agents in GOAL . In: Bordini et al. [65], chap. 4, pp. 119–157
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)
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)
Hindriks, K.V., Roberti, T.: Goal as a planning formalism. In: Proceedings of MATES 2009 (2009)
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)
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)
Newell, A.: The Knowledge Level . Artificial Intelligence 18(1), 87–127 (1982)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
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)
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)
de Bakker, J.: Mathematical Theory of Program Correctness. Prentice Hall, Inc. (1980)
Shapiro, S., Lespérance, Y., Levesque, H.J.: Goal change in the situation calculus. Journal of Logic and Computation 17(5), 983–1018 (2007)
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)
Plotkin, G.D.: A Structural Approach to Operational Semantics . Tech. Rep. DAIMI FN-19, University of Aarhus (1981)
Thiébaux, S., Hoffmann, J., Nebel, B.: In defense of PDDL axioms . Artificial Intelligence 168, 38–69 (2005)
Dastani, M.: 2APL : A practical agent programming language. Autonomous Agents and Multi-Agent Systems 16(3), 214–248 (2008)
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)