paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints

具有社会福利与时序逻辑约束的并发博弈均衡设计
LMCS vol.Volume 20, Issue 42024匹配度 2/10 · 论文属于形式化方法与博弈论中的均衡设计,涉及时序逻辑和并发博弈验证,与用户核心关注的静态分析、LLM/Agent 交叉、浮点程序分析或贝叶斯程序分析没有直接关联;仅与程序验证/时序逻辑方向有边缘联系。引用 0 inbox
Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge
crossref: 2026-09-10

AI 速览

一句话:提出均衡设计框架,通过激励使并发博弈的Nash均衡满足LTL/GR(1)时序性质,并给出复杂度界。

本文研究均衡设计:为并发博弈设计激励,使某个或所有Nash均衡满足给定时序逻辑性质。框架中系统规约用时序逻辑公式表示,博弈为定量并发博弈结构,玩家目标为平均收益。作者针对LTL和GR(1)规约,证明使某个或所有Nash均衡满足性质的激励设计问题分别属于PSPACE与NP/Σ₂ᴾ;并分析解的最优性、唯一性及社会福利等决策与优化问题,复杂度位于多项式谱系内。该框架可作为平均收益并发博弈在无解时进行理性合成与验证的替代方案,也可用于以最优方式修复具有不良Nash均衡的并发博弈。

问题
在并发博弈中,当不存在满足系统规约的Nash均衡时,如何通过设计激励来获得满足给定时序逻辑性质的理想均衡。
方法
将系统规约表示为LTL/GR(1),博弈建模为定量并发博弈结构,玩家目标为平均收益,并研究激励设计及相关决策与优化问题的计算复杂度。
评估
以理论复杂度分析为主,证明LTL情形的PSPACE上界、GR(1)情形的NP/Σ₂ᴾ上界,并给出最优性、唯一性与社会福利等问题的多项式谱系界。
原文摘要(Abstract)

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

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}