Abstract
Systems of autonomous agents providing automated services over the Web are fast becoming a reality. Often these agent systems are constructed using procedural architectures that provide a framework for connecting agent components that perform speci.c tasks. The agent designer codes the tasks necessary to perform a service and uses the framework to connect the tasks into an integrated agent structure. This bottom up approach does not provide an easy mechanism for con.rming global properties of constructed agent systems. In this paper we propose a declarative methodology based on logic programming for modeling such procedurally constructed agents and specifying their global properties as temporal logic formulas. This methodology allows us to bring to bear a body of work for using logic programming based model checking to verify certain global properties of procedurally constructed Multi-Agent Systems.
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
Business process execution language for web sevices (BPEL4WS), http://www.ibm.com/developerworks/library/ws-bpel/
Cougaar: Cognitive agent architecture, http://www.cougaar.org
Alferes, J., Brogi, A., Leite, J.A., Pereira, L.M.: Logic programming for evolving agents. In: Klusch, M., Omicini, A., Ossowski, S., Laamanen, H. (eds.) CIA 2003. LNCS (LNAI), vol. 2782, pp. 281–297. Springer, Heidelberg (2003)
Baldoni, M., et al.: Reasoning about communicating agents inside DCaseLP. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 112–131. Springer, Heidelberg (2005)
Basu, S., Kumar, K.N., Pokorny, L.R., Ramakrishnan, C.R.: Resource-constrained model checking of recursive programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 236–250. Springer, Heidelberg (2002)
Bhat, G., Cleaveland, R., Groce, A.: Efficient model checking via beuchi tabeau automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 38. Springer, Heidelberg (2001)
Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL*. In: IEEE Symposium on Logic in Computer Science. IEEE Press, Los Alamitos (1995)
Bonner, A., Kifer, M.: An overview of transaction logic. Theoretical Computer Science 133, 205–265 (1994)
Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model checking AgentSpeak. In: Second Internatonal Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS) (2003)
Chopra, A.K., Mallya, A.U., Desai, N.V., Singh, M.P.: Modeling flexible business processes. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476. Springer, Heidelberg (2005)
Davulcu, H., Kifer, M., Ramakrishnan, C.R., Ramakrishnan, I.V.: Logic based modeling and analysis of workflows. In: ACM Symposium on Principles of Database Systems (PODS), pp. 25–33. ACM, New York (1998)
Du, X., Ramakrishnan, C.R., Smolka, S.A.: Tabled resolution + constraints: A recipe for model checking real-time systems. In: IEEE Real Time Systems Symposium (RTSS), Orlando, Florida (2000)
Eshuis, R.: Semantics and Verification of UML Activity Diagrams for Workflow Modelling. PhD thesis, University of Twente (2002)
Fan, X., Yen, J., Miller, M., Volz, R.: The semantics of MALLET — an agent teamwork encoding language. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 69–91. Springer, Heidelberg (2005)
Kifer, M., Lausen, G., Wu, J.: Logical foundations of object-oriented and frame-based languages. Journal of the ACM 42(4), 741–843 (1995)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)
Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)
Pokorny, L.R., Ramakrishnan, C.R.: Model checking linear temporal logic using tabled logic programming. In: Workshop on Tabling in Parsing and Deduction (TAPD) (2000)
Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T.L., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
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 (LNAI), vol. 1038, pp. 42–55. Springer, Heidelberg (1996)
Robertson, D.: A lightweight coordination calculus for agent social norms. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 183–197. Springer, Heidelberg (2005)
Sarna-Starosta, B., Ramakrishnan, C.R.: Constraint based model checking of data independent systems. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 579–598. Springer, Heidelberg (2003)
Subrahmanian, V.S., Bonatti, P., Dix, J., Eiter, T., Kraus, S., Ozcan, F.: Heterogenous Agent Systems. MIT Press, Cambridge (2000)
Vasconcelos, W.W.: Norm verification and analysis of electronic institutions. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 166–182. Springer, Heidelberg (2005)
Walton, C.: Model checking agent dialogues. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 132–147. Springer, Heidelberg (2005)
Wooldridge, M., Fisher, M., Huget, M.-P., Parsons, S.: Model checking multi-agent systems with MABLE. In: First Internatonal Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 952–959. ACM Press, New York (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pokorny, L.R., Ramakrishnan, C.R. (2005). Modeling and Verification of Distributed Autonomous Agents Using Logic Programming. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds) Declarative Agent Languages and Technologies II. DALT 2004. Lecture Notes in Computer Science(), vol 3476. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11493402_9
Download citation
DOI: https://doi.org/10.1007/11493402_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26172-8
Online ISBN: 978-3-540-31927-6
eBook Packages: Computer ScienceComputer Science (R0)