Some Decidable classes of the distributed synthesis problem[HBNI Th128]

Abstract

In this thesis we study the distributed synthesis problem, which asks for an algorithm that synthesizes distributed systems from a given specification. We study this via the equivalent problem of determining the winning strategy of multi-player imperfect information games. More concretely, is there an algorithm, that given a multi-player imperfect information game as a game graph and a regular winning condition on the plays of the game, determines the existence of a winning strategy. The above problem is known to be undecidable, even for very simple winning conditions.

The contribution of this thesis is in determining new decidable classes of games. In particular, we show that the winning strategy problem is decidable for the following:

1. Imperfect information games with Recurring Common Knowledge of State: This condition relies on the fact that bounded common knowledge among the players of the game, leads to effective algorithms for the winning strategy problem. We show that under this condition, the existence of winning strategy can be decided in NEXPTIME and winning strategies can be synthesized in 2EXPTIME.

2. Imperfect information games with Retractable Witnesses: We identify a generic approach to solving the winning strategy problem, which comprises of two steps:

first, we define a notion of a witness, the existence of which implies the existence of winning strategy; second, we define an operation called retraction, that can transform a witnesses into bounded-size witnesses. We then show that for classes of games whose witnesses admit a retraction to bounded-size witnesses, the existence of winning strategy can be determined. Using this approach, we solve the following classes of games:

(a) Imperfect information games with no Fork-Triples: We define a property of games called fork-triple, the absence of which is a favorable criterion to decide the winning strategy problem. We show that in this case, the winning strategy problem is decidable with an algorithm whose complexity is non-elementary in the size of the inputs. We also show that the condition of absence of fork-triples on games is satisfied by many classes of games previously known to be decidable.

(b) Imperfect information games obtained from Modular-Broadcast Architectures: We show that games obtained from modular-broadcast architectures admit a decidable winning strategy problem, when restricted to local winning condition. Here again the complexity of the algorithm is non-elementary in the size of the inputs and includes all previously known decidable classes of games with local winning conditions.