Verifying Space and Time Requirements for Resource-Bounded Agents

  • Natasha Alechina
  • Piergiorgio Bertoli
  • Chiara Ghidini
  • Mark Jago
  • Brian Logan
  • Luciano Serafini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)


The effective reasoning capability of an agent can be defined as its capability to infer, within a given space and time bound, facts that are logical consequences of its knowledge base. In this paper we show how to determine the effective reasoning capability of an agent with limited memory by encoding the agent as a transition system and automatically verifying whether a state where the agent believes a certain conclusion is reachable from the start state. We present experimental results using the Model Based Planner (mbp) which illustrates how the length of the deduction varies for different memory sizes.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ågotnes, T., Walicki, M.: Complete axiomatizations of finite syntactic epistemic states. In: Baldoni, M., Endriss, U., Omicini, A., Torroni, P. (eds.) DALT 2005. LNCS (LNAI), vol. 3904, pp. 33–50. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Alechina, N., Logan, B., Whitsey, M.: A complete and decidable logic for resource-bounded agents. In: Proceedings of the Third International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2004), pp. 606–613. ACM Press, New York (July 2004)Google Scholar
  3. 3.
    Benerecetti, M., Giunchiglia, F., Serafini, L.: Model Checking Multiagent Systems. Journal of Logic and Computation, Special Issue on Computational & Logical Aspects of Multi-Agent Systems 8(3), 401–423 (1998)zbMATHMathSciNetGoogle Scholar
  4. 4.
    Berger, M., Bauer, B., Watzke, M.: A scalable agent infrastructure. In: Proceedings of the Second Workshop on Infrastructure for Agents, MAS and Scalable MAS (held in conjuction with Autonomous Agents’01), Montreal (2001)Google Scholar
  5. 5.
    Bibel, W.: A deductive solution for plan generation. New Generation Computing 4, 115–132 (1986)zbMATHCrossRefGoogle Scholar
  6. 6.
    Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking. Artificial Intelligence 147(1,2), 35–84 (2003)zbMATHMathSciNetGoogle Scholar
  7. 7.
    Duc, H.N.: Reasoning about rational, but not logically omniscient, agents. Journal of Logic and Computation 7(5), 633–648 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Elgot-Drapkin, J., Miller, M., Perlis, D.: Memory, reason and time: the Step-Logic approach. In: Philosophy and AI: Essays at the Interface, pp. 79–103. MIT Press, Cambridge, Massachusetts (1991)Google Scholar
  9. 9.
    Elgot-Drapkin, J.J., Perlis, D.: Reasoning situated in time I: Basic concepts. Journal of Experimental and Theoretical Artificial Intelligence 2, 75–98 (1990)CrossRefGoogle Scholar
  10. 10.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge, Massachusetts (1995)zbMATHGoogle Scholar
  11. 11.
    Fikes, R.E., Nilsson, N.J.: STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence 2, 187–208 (1971)CrossRefGoogle Scholar
  12. 12.
    Fisher, M., Ghidini, C.: Programming Resource-Bounded Deliberative Agents. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI 1999), pp. 200–206. Morgan Kaufmann, San Francisco (1999)Google Scholar
  13. 13.
    Horrocks, I., Patel-Schneider, P.F.: A proposal for an OWL rules language. In: Proceedings of the 13th international conference on World Wide Web, WWW 2004, pp. 723–731. ACM, New York (2004)CrossRefGoogle Scholar
  14. 14.
    Jacopin, E.: Classical AI planning as theorem proving: The case of a fragment of linear logic. In: AAAI Fall Symposium on Automated Deduction in Nonstandard Logics, pp. 62–66. AAAI Press, Palo Alto, California (1993)Google Scholar
  15. 15.
    Kacprzak, M., Lomuscio, A., Penczek, W.: Verification of multiagent systems via unbounded model checking. In: Kudenko, D., Kazakov, D., Alonso, E. (eds.) Adaptive Agents and Multi-Agent Systems II(AAMAS). LNCS (LNAI), vol. 3394, Springer, Heidelberg (2005)Google Scholar
  16. 16.
    Kautz, H., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: Proceedings of the Thirteenth National Conference on Artificial Intelligence, pp. 1194–1201. AAAI Press, Stanford, California, USA (1996)Google Scholar
  17. 17.
    Russell, S.J.: Rationality and intelligence. Artificial Intelligence 94(1-2), 57–77 (1997)zbMATHCrossRefGoogle Scholar
  18. 18.
    Tarkoma, S., Laukkanen, M.: Supporting software agents on small devices. In: Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), pp. 565–566. ACM Press, New York, NY, USA (2002)CrossRefGoogle Scholar
  19. 19.
    van Benthem, J., Liu, F.: Diversity of agents in games. Philosophia Scientiae, vol. 8(2) (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Natasha Alechina
    • 1
  • Piergiorgio Bertoli
    • 2
  • Chiara Ghidini
    • 2
  • Mark Jago
    • 1
  • Brian Logan
    • 1
  • Luciano Serafini
    • 2
  1. 1.School of Computer Science, University of Nottingham, NottinghamUK
  2. 2.ITC-IRST, TrentoItaly

Personalised recommendations