Swarup K. Mohalik: DGames for Distributed Controller Synthesis

Abstract: Given a system consisting of a process, an environment and possible ways of interaction among them, the synthesis problem is stated as follows: given a specification S, find a finite state program P for the process such that the overall behaviour of the system satisfies S, no matter how the environment behaves. Starting from the works of Ramadge and Wonham[RW], discrete control synthesis problem has been solved using many different approaches[PR1, AVW].

The synthesis problem above has been extended to a distributed setting where there are multiple processes and interactions among processes along with interaction of processes with the environment. Here, one has to find a finite state program P for each of the processes so that the overall behaviour satisfies a given specification. In contrast to the centralized synthesis problem, distributed synthesis has been shown to be a hard problem and is undecidable for a most natural style of formulation called Architectural Synthesis [PR, KV, Mad, FS]. A crucial observation is that in this setting, one can write specifications which will force the synthesis solution to encode the halting problem of Turing machines.

However, since the synthesis problem starts with a given specification, which is usually not very complex, the formulation of the synthesis problem can take advantage of the specification itself. With this as one of the motivations, we have suggested a framework based upon Game theory to encode the distributed synthesis problem.

In the case of centralized synthesis, an interaction of the process with its environment is seen as a game between two players[ALW, PR2,Tho]. The synthesis problem is then reduced to finding a finite state winning strategy for the process. We extend the definition of two player games to multi-player ones : we call them distributed games [MW]. We also show two theorems that simplify the distributed games by reducing the number of players and reducing the non-determinism in the game. We illustrate how in some cases the simplification can reduce the multi-player distributed game to a two player game which is decidable by the classical results. The hope is that the joint representation of the interactions and the specification will lead to such simplifiable distributed games. A complete characterization of such games is still an open question.


Bio: Swarup Kumar Mohalik obtained his PhD degree in Computer Science from Institute of Mathematical Science, Chennai, India in 1999. He worked in the R&D division of Sasken Communication Technologies Limited, Bangalore as a research scientist till 2001. During 2001-2003 he earned a post-doctoral fellowship in LABRI, University of Bordeaux, France. He was a member of the HP Labs during 2004-2006. Since then he is working as a senior researcher in the India Science Lab for General Motors. He specializes in the areas of formal verification and discrete control synthesis and has worked in domains of communication protocols, semantic networks and automotive systems.

Appointments: dcm@cs.cmu.edu


Maintainer Home > Seminar ]
`Last modified: Thurs Oct 11 11:09:10 EDT 2007