Alladi Ramakrishnan Hall
Some Decidable Classes of the Distributed Synthesis Problem
Anup Basil Mathew
IMSc
*** This is the Public Viva Voce Examination of Anup's Ph D Thesis submission. ***
The distributed synthesis problem (or DSP) is the
following: Given an architecture and a property as input, find a distributed system on the architecture that satisfies the given property.
It is known that DSP is undecidable even for 'simple' input-classes, but some input-classes that admit a decidable DSP have also been identified. In this thesis, we identify more input-classes with decidable DSP.
The results are summarized below:
1. We show that on inputs that admit the property of recurring common knowledge of state", DSP reduces to the winning strategy problem on perfect information game-graphs, which is a known decidable problem.
2. We consider several input-classes, some of which are from the literature, and give a uniform argument for their decidability. The idea can be summarized as follows: first, we define a structure called
a "witness" that witnesses a distributed system associated with an input; second, for each input-class being considered, we show that the witnesses
associated with an input admit a transformation to bounded-size witnesses,
and decidability follows from this.
Done