A logic for strategic reasoning

ABSTRACT

Rational strategic reasoning is the process whereby an agent reasons about the best strategy to adopt in a given multi-agent scenario, taking into account the likely behaviour of other participants in the scenario, and, in particular, how the agent's choice of strategy will affect the choices of others. We present CATL, a logic that is intended to facilitate such reasoning. CATL is an extension of Alternating-time Temporal Logic (ATL), which supports reasoning about the abilities of agents and their coalitions in game-like multi-agent systems. CATL extends ATL with a ternary counterfactual commitment operator of the form Ci(σ, φ), with the intended reading "if it were the case that agent i committed to strategy σ, then φ". By using this operator in combination with the ability operators of ATL, it is possible to reason about the implications of different possible choices by agents. We illustrate the approach by showing how CATL may be used to express properties of games such as Nash equilibrium and Pareto efficiency. We also show that the model checking problem for CATL is tractable, and hence that efficient implementations of strategic reasoners based on CATL are feasible.

REFERENCES

• 1: 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
• 2: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002 [doi>10.1145/585265.585270]
• 3: A. Baltag. A logic for suspicious players. Bulletin of Economic Research, 54(1):1--46, 2002.
• 4: J. van Benthem. Games in dynamic epistemic logic. Bulletin of Economic Research, 53(4):219--248, 2001. Proceedings of LOFT-4.
• 5: Johan Van Benthem, Extensive Games as Process Models, Journal of Logic, Language and Information, v.11 n.3, p.289-313, Summer 2002 [doi>10.1023/A:1015534111901 ]
• 6: Avrim L. Blum , Merrick L. Furst, Fast planning through planning graph analysis, Artificial Intelligence, v.90 n.1-2, p.281-300, Feb. 1997 [doi>10.1016/S0004-3702(96)00047-1 ]
• 7: G. Bonanno. Branching time logic, perfect information games and backward induction. Games and Economic Behavior, 36(1):57--73, July 2001.
• 8: Govert van Drimmelen, Satisfiability in Alternating-time Temporal Logic, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.208, June 22-25, 2003
• 9: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 10: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 11: V. Goranko and W. Jamroga. Comparing semantics of logics for multi-agent systems. Synthese, 139(2):241--280, 2004.
• 12: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 13: P. Harrenstein, W. van der Hoek, J.-J Meyer, and C. Witteveen. On modal logic interpretations for games. In Proceedings of the Fifteenth European Conference on Artificial Intelligence (ECAI-2002), pages 28--32, Lyon, France, 2002.
• 14: W. van der Hoek, M. Roberts, and M. Wooldridge. Social laws in alternating time: Effectiveness, feasibility and synthesis. Synthese, 2005.
• 15: W. Jamroga, W. van der Hoek, and M. Wooldridge. Intentions and strategies in game-like scenarios. Technical Report IfI-05-08, Clausthal University of Technology, 2005.
• 16: N. R. Jennings. Commitments and conventions: The foundation of coordination in multi-agent systems. The Knowledge Engineering Review, 8(3):223--250, 1993.
• 17: D. Lewis. Counterfactuals. Blackwells: Oxford, 1973.
• 18: M. J. Osborne and A. Rubinstein. A Course in Game Theory. The MIT Press: Cambridge, MA, 1994.
• 19: M. Pauly. A modal logic for coalitional power in games. Journal of Logic and Computation, 12(1):149--166, 2002.
• 20: A. S. Rao and M. P. Georgeff. Modeling rational agents within a BDI-architecture. In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, pages 473--484, 1991.
• 21: P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2), 2004.
• 22: R. Stalnaker. Knowledge, belief and counterfactual reasoning in games. Economics and Philosophy, 12:133--163, 1996.
• 23: Sieuwert van Otterloo , Wiebe van der Hoek , Michael Wooldridge, Preferences in Game Logics, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.152-159, July 19-23, 2004, New York, New York [doi>10.1109/AAMAS.2004.214]
• 24: M. Wooldridge. Reasoning about Rational Agents. The MIT Press: Cambridge, MA, 2000.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Theory

Keywords:
game theory, modal logic, multi-agent systems, strategic reasoning