Contract-Based Distributed Synthesis in Two-Objective Parity Games

We present a novel method to compute textitassume-guarantee contracts in non-zerosum two-player games over finite graphs where each player has a different ω -regular winning condition. Given a game graph G and two parity winning conditions Phi0 and Phi1 over G, we compute textitcontracted strategy-masks (textttcsm) (Psii,Phii) for each Player i. Within a textttcsm, Phii is a textitpermissive 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 textitpermissive assumption template Psii. The main feature of textttcsm's is their power to textitfully decentralize all remaining strategy choices -- if the two player's textttcsm's are compatible, they provide a pair of new local specifications Phi0^bullet and Phi1^bullet such that Player i can locally and fully independently choose any strategy satisfying Phii^bullet and the resulting strategy profile is ensured to be winning in the original two-objective game (G,Phi0,Phi1). In addition, the new specifications Phii^bullet are textitmaximally cooperative, i.e., allow for the distributed synthesis of any cooperative solution. Further, our algorithmic computation of textttcsm'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 enquotecorrect-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.