Madhavan Mukund

From global specifications to distributed implementations

M Mukund

Synthesis and Control of Discrete Event Systems, B. Caillaud, P. Darondeau, L. Lavagno (eds), Kluwer (2002) 19-34.

Invited talk presented at the Workshop on Synthesis of Concurrent Systems, a satellite event of the International Conference on Applications and Theory of Petri Nets (ICATPN) held in Newcastle, U.K., in June 2001.


We study the problem of synthesizing distributed implementations from global specifications. We work in the framework of transition systems. The main question we address is the following.

Given a global transition system TS over a set of actions Σ together with a distribution of Σ into local components (Σ12,…,Σk), does there exist a distributed transition system over (Σ12,…,Σk) that is ``equivalent'' to TS?

We focus on two different types of distributed transition systems---loosely cooperating systems and synchronously communicating systems. For ``equivalence'' we consider three possibilities---state-space isomorphism, language equivalence and bisimulation.

We survey the current state of knowledge about the different versions of the problem that arise from choosing a concrete notion of equivalence and a specific model of distributed transition systems.

  • Download PDF.