Logics for strategic reasoning and collective decision-making

Abstract

Strategic decision-making is ubiquitous in everyday life. The analysis of game strategies has been a research theme in game theory for several decades since von Neumann and Morgenstern. Sophisticated models and analysis tools have been developed with wide applications in Economics, Management Science, Social Science and Computer Science, especially in the field of Artificial Intelligence. However, \\much of game theory is about the question whether strategic equilibria exist", as Johan van Benthem, a world-leading logician and game-theorist, points out, \\but there are hardly any explicit languages for defining, comparing, or combining strategies". Without such a facility it is challenging for computer scientists to build intelligent agents that are capable of strategic decision-making. In the last twenty years, logical approaches have been proposed to tackle this problem. Pioneering work includes Game Logics, Coalition Logic and Alternating-time Temporal Logic (ATL). These logics either provide facilities for expressing and combining games or offer mechanisms for reasoning about strategic abilities of players. But none of them can solve the problem. The intrinsic difficulty in establishing such a logic is that reasoning about strategies requires combinations of temporal reasoning, counterfactual reasoning, reasoning about actions, preferences and knowledge, as well as reasoning about multi-agent interactions and coalitional abilities. More recently, a few new logical formalisms have been proposed by extending ATL with strategy variables in order to express strategies explicitly. However, most of these logics tend to have high computational complexity, because ATL introduces quantifications over strategies (functions), which leaves little hope of building any tractable inference system based on such a logic. This thesis takes up the challenge by using a bottom-up approach in order to create a balance between expressive power and computational efficiency. Instead of starting with a highly complicated logic, we propose a set of logical frameworks based on a simple and practical logical language, called Game Description Language (GDL), which has been used as an official language for General Game Playing (GGP) since 2005. To represent game strategies, we extend GDL with two binary prioritized connectives for combining actions in terms of their priorities specified by these connectives, and provide it with a semantics based on the standard state transition model. To reason about the strategic abilities of players, we further extend the framework with coalition operators from ATL for specifying the strategic abilities of players. More importantly, a unified semantics is provided for both GDL- and ATL- formulas, which allows us to verify and reason about game strategies. Interestingly, the framework can be used to formalize the fundamental game-playing principles and formally derive two well-known results on two-player games: Weak Determinacy and Zermelo's Theorem. We also show that the model-checking problem of the logic is not worse than that of ATL*, an extension of ATL. To deal with imperfect information games, we extend GDL with the standard epistemic operators and provide it with a semantics based on the epistemic state transition model. The language allows us to specify an imperfect information game and formalize its epistemic properties. Meanwhile, the framework allows us to reason about players' own as well as other players' knowledge during game playing. Most importantly, the logic has a moderate computational complexity, which makes it significantly different from similar existing frameworks. To investigate the interplay between knowledge shared by a group of players and its coalitional abilities, we provide a variant of semantics for ATL with imperfect information. The relation between knowledge sharing and coalitional abilities is investigated through the interplay of epistemic and coalition modalities. Moreover, this semantics is able to preserve the desirable properties of coalitional abilities. To deal with collective decision-making, we apply the approach of combining actions via their priorities for collective choice. We extend propositional logic with the prioritized connective for modelling reason-based individual and collective choices. Not only individual preferences but also aggregation rules can be expressed within this logic. A model-checking algorithm for this logic is thus developed to automatically generate individual and collective choices. In many real-world situations, a group making collective judgments may assign individual members or subgroups different priorities to determine the collective judgment. We design an aggregation rule based on the priorities of individuals so as to investigate how the judgment from each individual affects group judgment in a hierarchical environment. We also show that this rule satisfies a set of plausible conditions and has a tractable computational complexity.

Date of Award	2016
Original language	English