Contract-Based Distributed Synthesis in Two-Objective Parity Games

Abstract

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.