一句话:提出均衡设计框架,通过激励使并发博弈的Nash均衡满足LTL/GR(1)时序性质,并给出复杂度界。
本文研究均衡设计:为并发博弈设计激励,使某个或所有Nash均衡满足给定时序逻辑性质。框架中系统规约用时序逻辑公式表示,博弈为定量并发博弈结构,玩家目标为平均收益。作者针对LTL和GR(1)规约,证明使某个或所有Nash均衡满足性质的激励设计问题分别属于PSPACE与NP/Σ₂ᴾ;并分析解的最优性、唯一性及社会福利等决策与优化问题,复杂度位于多项式谱系内。该框架可作为平均收益并发博弈在无解时进行理性合成与验证的替代方案,也可用于以最优方式修复具有不良Nash均衡的并发博弈。
In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we explore the concept of equilibrium design, where incentives are designed to obtain a desirable equilibrium that satisfies a specific temporal logic property. Our study is based on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. We consider system specifications given by LTL and GR(1) formulae, and show that designing incentives to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game can be achieved in PSPACE for LTL properties and in NP/{\Sigma}P 2 for GR(1) specifications. We also examine the complexity of related decision and optimisation problems, such as optimality and uniqueness of solutions, as well as considering social welfare, and show that the complexities of these problems lie within the polynomial hierarchy. Equilibrium design can be used as an alternative solution to rational synthesis and verification problems for concurrent games with mean-payoff objectives when no solution exists or as a technique to repair concurrent games with undesirable Nash equilibria in an optimal way.Comment: arXiv admin note: substantial text overlap with arXiv:2106.10192
@article{paperbot2701,
title = {Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints},
author = {Julian Gutierrez and Muhammad Najib and Giuseppe Perelli and Michael Wooldridge},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:21)2024}
}