Tractable multiagent planning for epistemic goals

ABSTRACT

An epistemic goal is a goal about the knowledge possessed by an agent or group of agents. In this paper, we address the problem of how plans might be developed for a group of agents to cooperate to bring about such a goal. We present a novel approach to this problem, in which the problem is formulated as one of model checking in Alternating Temporal Epistemic Logic (ATEL). After introducing this logic, we present a model checking algorithm for it, and show that the model checking problem for this logic is tractable. We then show how multiagent planning can be treated as a model checking problem in ATEL, and discuss the related issue of checking knowledge preconditions for multiagent plans. We illustrate the approach with an example. We then describe how this example was implemented using the MOCHA model checking system, and conclude by discussing the relationship of our work with that of others in the planning and speech acts communities.

REFERENCES

• 1: R. Alur, L. de Alfaro, T. A. Henzinger, S. C. Krishnan, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Taşiran. mocha user manual. University of Berkeley Report, 2000.
• 2: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 3: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time Temporal Logic, Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97), p.100, October 19-22, 1997
• 4: A. Baltag. A logic for supicious players. Bulletin of Economic Research, 54(1):1--45, 2002.
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: H.P. van Ditmarsch. Knowledge Games. PhD thesis, University of Groningen, Groningen, 2000.
• 7: S. Druiven. Opponent modeling and dynamic epistemic logic in games with imperfect information. M.Sc. thesis, in preparation, 2002.
• 8: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 9: Kai Engelhardt , Ron van der Meyden , Yoram Moses, Knowledge and the logic of local propositions, Proceedings of the 7th conference on Theoretical aspects of rationality and knowledge, July 22-24, 1998, Evanston, Illinois
• 10: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 11: Fausto Giunchiglia , Paolo Traverso, Planning as Model Checking, Proceedings of the 5th European Conference on Planning: Recent Advances in AI Planning, p.1-20, September 08-10, 1999
• 12: Wiebe van der Hoek , Michael Wooldridge, Model Checking Knowledge and Time, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.95-111, April 11-13, 2002
• 13: B. van Linder, W. van der Hoek, and J.-J. Ch. Meyer. Actions that make you change your mind. In A. Laux and H. Wansing, editors, Knowledge and Belief in Philosophy and AI, pages 103--146. Akademie-Verlag, 1995.
• 14: John-Jules Ch Meyer , Wiebe Van Der Hoek, Epistemic Logic for AI and Computer Science, Cambridge University Press, New York, NY, 1995
• 15: M. Pauly. A logical framework for coalitional effectivity in dynamic procedures. Bulletin of Economic Research, 53(4):305--324, 2002.
• 16: Amir Pnueli , Roni Rosner, On the Synthesis of an Asynchronous Reactive Module, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.652-671, July 11-15, 1989
• 17: Jeffrey S. Rosenschein , Gilad Zlotkin, Rules of encounter: designing conventions for automated negotiation among computers, MIT Press, Cambridge, MA, 1994
• 18: Moshe Y. Vardi, Branching vs. Linear Time: Final Showdown, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.1-22, April 02-06, 2001
• 19: M. Wooldridge, C. Dixon, and M. Fisher. A tableau-based proof method for temporal logics of knowledge and belief. Journal of Applied Non-Classical Logics, 8(3):225--258, 1998.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods
          Subjects: Modal logic

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods
          Subjects: Temporal logic

General Terms:
Theory, Verification

Keywords:
epistemic & temporal logic, model checking, planning