A Retraction Theorem for Distributed Synthesis

TL;DR

This paper introduces a general retraction theorem for distributed synthesis in coordination games with omega-regular objectives, enabling solutions when agents' knowledge remains bounded despite imperfect information.

Contribution

It provides a new theoretical framework for distributed synthesis, characterizing decidability through bounded knowledge states and finite congruence classes.

Findings

Existence of an 'essential' winning strategy derived by retraction.

Decidability linked to bounded knowledge states and finite congruence classes.

Applicable to games with unobservable objectives in imperfect information settings.

Abstract

We present a general theorem for distributed synthesis problems in coordination games with $\omega$-regular objectives of the form: If there exists a winning strategy for the coalition, then there exists an "essential" winning strategy, that is obtained by a retraction of the given one. In general, this does not lead to finite-state winning strategies, but when the knowledge of agents remains bounded, we can solve the synthesis problem. Our study is carried out in a setting where objectives are expressed in terms of events that may \emph{not} be observable. This is natural in games of imperfect information, rather than the common assumption that objectives are expressed in terms of events that are observable to all agents. We characterise decidable distributed synthesis problems in terms of finiteness of knowledge states and finite congruence classes induced by them.