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以及两个奇偶获胜条件Φ₀和Φ₁，我们为每个博弈方i计算名为紧缩策略掩码（csm）(Ψᵢ, Φᵢ)。在每个csm中，Φᵢ是一个宽松策略模板，该模板收集了博弈方i在假设博弈方1-i从宽松假设模板Ψᵢ中选择任意策略时可使用的无数获胜策略。csm的主要特点在于其能够完全分散所有剩余策略选择——如果两个博弈方的csm相互兼容，它们会提供一组新的局部规范Φ₀ᵌ和Φ₁ᵌ，使得博弈方i可以完全独立地本地选择任何满足Φᵢᵌ的策略，且由此生成的策略组合在原始双目标博弈(G, Φ₀, Φ₁)中保证获胜。此外，新规范Φᵢᵌ具有最大合作性，即允许对任何合作解决方案进行分布式综合。进一步地，我们提出的csm算法计算是完备的且保证终止。我们通过实例说明了该综合框架的独特特性如何有效应对信息物理系统中“正确性保障”逻辑控制软件综合的多项挑战，并提供经验证据表明，与现有先进技术相比，本方法在结构性和计算性方面均具备理想性质。