SEAL · Strategic reasoning for socially good mechanisms

Strategic reasoning for socially good mechanisms

The design and evaluation of games (also known as mechanisms) for aggregating preferences is a central problem in Multi-Agent Systems (MAS). In such a setting, we need to be able to aggregate individual preferences, which are conflicting when agents are self-interested. More importantly, the mechanism should choose a socially desirable (or “good”) outcome and reach an equilibrium even though agents can lie about their preferences. For instance, an election is a mechanism that combines agents' votes into the choice of one or several winning candidates. The main issues in designing such a mechanism are to motivate a desirable behavior of strategic voters and to ensure characteristics regarding the quality of the joint decision. In particular, elections could be designed to avoid a dictatorship (a participant that chooses the result all by herself), to incentivize people to participate, to choose a winner that maximizes social welfare, and so on. The real-world applications of designing and verifying mechanisms for social choice are manifold, including the classic problems of auctions, markets, and government policies. Furthermore, new and trending applications include fair division protocols, secure voting, and truth-tracking via approval voting (i.e. unveiling a hidden ground truth given votes). In Automated Mechanism Design (AMD), the design of new mechanisms is treated as a computational optimization problem for specific preference aggregation settings and domains. Although logic-based languages have been widely used for verification and synthesis of MAS, the use of formal methods for reasoning about auctions under strategic behavior as well as automated mechanism design has not been much explored yet. An advantage of adopting such a perspective lies in the high expressivity and generality of logics for strategic reasoning. Moreover, by relying on precise semantics, formal methods provide tools for rigorously analyzing the correctness of systems, which is important to improve trust in mechanisms (fully or partially) created by machines. The problem of formally reasoning about mechanisms is, however, nontrivial: it requires considering quantitative information (e.g. utilities and payments), non-determinism, incomplete (e.g. Bayesian) and imperfect information about the participant’s preferences, and complex strategic concepts (such as strategy dominance and equilibria). The use of strategic logics developed for the verification of MAS as formal frameworks to reason about mechanism was advocated by Wooldridge et al.11. They consider the Alternating-time Temporal Logic (ATL), which has limitations to express some solution concepts as well to handle the quantitative aspects of mechanisms. As these are key features of mechanisms, Maubert et. al (21) recently proposed the use of variants of Strategy Logic (SL) for the verification and synthesis of deterministic mechanisms. This current approach has several limitations. First, as SL semantics is deterministic, the logic is unable to express probabilistic features, which are essential when considering Bayesian and randomized (or stochastic) mechanisms. Second, in the general setting, logics based on SL face decidability and complexity issues, which may prevent the practical use of such an approach. Finally, the works considered up to now were focused on auction mechanisms, which are usually designed for maximizing revenue. The validation of a logic-based approach for mechanism design requires investigating the feasibility of modeling other social choice problems as well as characterizing results and properties in those settings. This project aims to design a logical framework based on Strategy Logic for formally verifying and designing mechanisms for social choice. In particular, we aim to extend the existing approach of logic-based mechanism design to take into account the probabilistic setting (with Bayesian information, stochastic transitions, and mixed strategies), and identify fragments of SL that enjoy both good complexity and satisfying expressive power for being applied to classes of mechanisms. Additionally, we aim to model and reason about relevant problems from the state-of-the-art in computational social choice using the proposed logical framework.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз