Contract-Based Distributed Synthesis in Two-Objective Parity Games

We present a novel method to compute assume-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 Φ_0 and Φ_1 over G, we compute contracted strategy-masks () (Ψ_i,Φ_i) for each Player i. Within a , Φ_i is a 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 permissive assumption template Ψ_i. The main feature of 's is their power to fully decentralize all remaining strategy choices – if the two player's 's are compatible, they provide a pair of new local specifications Φ_0^∙ and Φ_1^∙ such that Player i can locally and fully independently choose any strategy satisfying Φ_i^∙ and the resulting strategy profile is ensured to be winning in the original two-objective game (G,Φ_0,Φ_1). In addition, the new specifications Φ_i^∙ are maximally cooperative, i.e., allow for the distributed synthesis of any cooperative solution. Further, our algorithmic computation of '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 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.