This paper considers the problem of co-synthesis in $k$-player games over a finite graph where each player has an individual $\omega$-regular specification $\phi_i$. In this context, a secure equilibrium (SE) is a Nash equilibrium w.r.t. the lexicographically ordered objectives of each player to first satisfy their own specification, and second, to falsify other players' specifications. A winning secure equilibrium (WSE) is an SE strategy profile $(\pi_i)_{i\in[1;k]}$ that ensures the specification $\phi:=\bigwedge_{i\in[1;k]}\phi_i$ if no player deviates from their strategy $\pi_i$. Distributed implementations generated from a WSE make components act rationally by ensuring that a deviation from the WSE strategy profile is immediately punished by a retaliating strategy that makes the involved players lose. In this paper, we move from deviation punishment in WSE-based implementations to a distributed, assume-guarantee based realization of WSE. This shift is obtained by generalizing WSE from strategy profiles to specification profiles $(\varphi_i)_{i\in[1;k]}$ with $\bigwedge_{i\in[1;k]}\varphi_i = \phi$, which we call most general winning secure equilibria (GWSE). Such GWSE have the property that each player can individually pick a strategy $\pi_i$ winning for $\varphi_i$ (against all other players) and all resulting strategy profiles $(\pi_i)_{i\in[1;k]}$ are guaranteed to be a WSE. The obtained flexibility in players' strategy choices can be utilized for robustness and adaptability of local implementations. Concretely, our contribution is three-fold: (1) we formalize GWSE for $k$-player games over finite graphs, where each player has an $\omega$-regular specification $\phi_i$; (2) we devise an iterative semi-algorithm for GWSE synthesis in such games, and (3) obtain an exponential-time algorithm for GWSE synthesis with parity specifications $\phi_i$.

翻译：本文研究有限图上$k$玩家博弈中的协同综合问题，其中每个玩家具有独立的$\omega$-正则规范$\phi_i$。在此背景下，安全均衡（SE）是指关于每个玩家词典序目标（首要满足自身规范，其次破坏其他玩家的规范）的纳什均衡。获胜安全均衡（WSE）是一种SE策略组合$(\pi_i)_{i\in[1;k]}$，使得当无玩家偏离其策略$\pi_i$时，能确保规范$\phi:=\bigwedge_{i\in[1;k]}\phi_i$成立。基于WSE生成的分布式实现通过确保偏离WSE策略组合的行为会立即遭到报复策略的惩罚（使相关玩家失败），从而促使组件理性运作。本文从基于WSE实现的偏离惩罚转向基于分布式假设-保证的WSE实现。这一转变通过将WSE从策略组合推广为规范组合$(\varphi_i)_{i\in[1;k]}$（满足$\bigwedge_{i\in[1;k]}\varphi_i = \phi$)来实现，我们称之为最大通用获胜安全均衡（GWSE）。此类GWSE具有如下性质：每个玩家可独立选择对$\varphi_i$获胜（对抗所有其他玩家）的策略$\pi_i$，且由此产生的所有策略组合$(\pi_i)_{i\in[1;k]}$必然构成WSE。策略选择空间的可获得灵活性可用于增强局部实现的鲁棒性与自适应性。具体而言，本文贡献有三点：(1) 形式化定义了有限图上$k$玩家博弈（每个玩家具有$\omega$-正则规范$\phi_i$）中的GWSE；(2) 设计了此类博弈中GWSE综合的迭代半算法；(3) 针对奇偶性规范$\phi_i$实现了指数时间复杂度的GWSE综合算法。