Print this page

One of the motivations for development of automata theory was the interest in verifying and synthesizing switching circuits. A circuit can be modeled as a function transforming infinite sequence of inputs into an infinite sequence of outputs. Church in 1963 has posed the problem of synthesizing such a function for a specification given in S1S, the monadic second order logic of one successor. The solution to this problem was given by Buchi and Ladweber in 1969. Nowadays we understand that this problem, and many other variations of the synthesis problem, reduce to finding a winning strategy in a two player game with perfect information and regular winning conditions.

A distributed system consist of some number of processes, each interacting in some way with the environment and other processes. The distributed synthesis problem is to find a program for each of the processes so that the global behaviour satisfies the given specification no matter what the behaviour of the environment is.

There are numerous ways of describing a distributed system and hence there are numerous ways of formalizing the distributed synthesis problem. One way, suggested by Pnueli and Rosner, is to consider a system as an architecture: a graph of communication channels connecting boxes into which we need to put I/O programs. The other way, introduced by Rudie and Wonham, is to specify the sets of controllable and observable actions for each of the components of the system. For these and other settings there are algorithms solving the distributed synthesis problem for some cases.

In the distributed synthesis we do not understand very well what makes the problem decidable or undecidable. Each decidability/undecidability proof depends very strongly on the formalism being used. One of the reasons for this is that, unlike for simple synthesis, we cannot reduce distributed synthesis problems to the problem of solving a two player game for a simple reason that in the distributed case there are more than two parties.

In this talk we will summarize the existing approaches to synthesis and distributed synthesis problems. We will propose a notion of distributed game that can serve as a common framework for distributed synthesis problems. In such a game there is one environment player and there is a coalition of process players, each having only a partial information about the play. We will state a couple of results on solvability of such games and indicate why they imply most of the known results for distributed synthesis problems.

© 2002-2003 Kurt Gödel Society, Norbert Preining.

2003-07-09