We present a novel method to compute $\textit{assume-guarantee contracts}$ in non-zerosum two-player games over finite graphs where each player has a different $ \omega $-regular winning condition. Given a game graph $G$ and two parity winning conditions $\Phi_0$ and $\Phi_1$ over $G$, we compute $\textit{contracted strategy-masks}$ ($\texttt{csm}$) $(\Psi_{i},\Phi_{i})$ for each Player $i$. Within a $\texttt{csm}$, $\Phi_{i}$ is a $\textit{permissive strategy template}$ which collects an infinite number of winning strategies for Player $i$ under the assumption that Player $1-i$ chooses any strategy from the $\textit{permissive assumption template}$ $\Psi_{i}$. The main feature of $\texttt{csm}$'s is their power to $\textit{fully decentralize all remaining strategy choices}$ -- if the two player's $\texttt{csm}$'s are compatible, they provide a pair of new local specifications $\Phi_0^\bullet$ and $\Phi_1^\bullet$ such that Player $i$ can locally and fully independently choose any strategy satisfying $\Phi_i^\bullet$ and the resulting strategy profile is ensured to be winning in the original two-objective game $(G,\Phi_0,\Phi_1)$. In addition, the new specifications $\Phi_i^\bullet$ are $\textit{maximally cooperative}$, i.e., allow for the distributed synthesis of any cooperative solution. Further, our algorithmic computation of $\texttt{csm}$'s is complete and ensured to terminate. We illustrate how the unique features of our synthesis framework effectively address multiple challenges in the context of \enquote{correct-by-design} logical control software synthesis for cyber-physical systems and provide empirical evidence that our approach possess desirable structural and computational properties compared to state-of-the-art techniques.

翻译：我们提出一种新方法，用于在有限图上的非零和两人博弈中计算假设-保证契约，其中每位玩家具有不同的ω-正则获胜条件。给定博弈图G及G上的两个偏序获胜条件Φ₀和Φ₁，我们为每位玩家i计算契约策略掩码（csm）(Ψᵢ, Φᵢ)。在csm中，Φᵢ是一个宽松策略模板，它收集了玩家i在假设玩家1-i从宽松假设模板Ψᵢ中选择任意策略时的无限多个获胜策略。csm的主要特征在于其完全分散所有剩余策略选择的能力——若两位玩家的csm相容，则它们能提供一对新的局部规约Φ₀ᐧ和Φ₁ᐧ，使得玩家i可局部且完全独立地选择满足Φᵢᐧ的任意策略，且由此产生的策略组合能确保在原始双目标博弈(G, Φ₀, Φ₁)中获胜。此外，新规约Φᵢᐧ具有最大合作性，即允许对任意合作解进行分布式综合。同时，我们提出的csm算法计算是完备的且保证终止。我们通过实例展示了该综合框架的独特特征如何有效应对信息物理系统中"正确性-by-设计"逻辑控制软件综合的多种挑战，并通过实证证明：与现有最优技术相比，该方法在结构和计算性质上具有显著优势。