English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a novel method to compute $\textit{assume-guarantee contracts}$ innon-zerosum two-player games over finite graphs where each player has adifferent $ \omega $-regular winning condition. Given a game graph $G$ and twoparity winning conditions $\Phi_0$ and $\Phi_1$ over $G$, we compute$\textit{contracted strategy-masks}$ ($\texttt{csm}$) $(\Psi_{i},\Phi_{i})$ foreach Player $i$. Within a $\texttt{csm}$, $\Phi_{i}$ is a $\textit{permissivestrategy template}$ which collects an infinite number of winning strategies forPlayer $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 remainingstrategy choices}$ -- if the two player's $\texttt{csm}$'s are compatible, theyprovide a pair of new local specifications $\Phi_0^\bullet$ and$\Phi_1^\bullet$ such that Player $i$ can locally and fully independentlychoose any strategy satisfying $\Phi_i^\bullet$ and the resulting strategyprofile 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{maximallycooperative}$, i.e., allow for the distributed synthesis of any cooperativesolution. Further, our algorithmic computation of $\texttt{csm}$'s is completeand ensured to terminate.  We illustrate how the unique features of our synthesis framework effectivelyaddress multiple challenges in the context of \enquote{correct-by-design}logical control software synthesis for cyber-physical systems and provideempirical evidence that our approach possess desirable structural andcomputational properties compared to state-of-the-art techniques.

Contract-Based Distributed Synthesis in Two-Objective Parity Games