From Global Specifications to Distributed Implementations

  • Madhavan Mukund


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 〈Σ1, ... , Σ k 〉, does there exist a distributed transition system over 〈Σ1, ... , Σ 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.


Transition System Synthesis Problem Label Transition System Product Language Discrete Event System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Arnold: Finite transition systems and semantics of communicating systems, Prentice-Hall (1994).Google Scholar
  2. [2]
    E. Badouel and Ph. Darondeau: Theory of Regions. Lectures on Petri nets I (Basic Models), LNCS 1491 (1998) 529–588.Google Scholar
  3. [3]
    I. Castellani, M. Mukund and P.S. Thiagarajan: Synthesizing distributed transition systems from global specifications, Proc. FSTTCS 19, LNCS 1739 (1999) 219–231.MathSciNetGoogle Scholar
  4. [4]
    W. Ebinger, A. Muscholl: Logical definability on infinite traces, Theor. Comput. Sci., 154 (1996) 67–84.MathSciNetzbMATHCrossRefGoogle Scholar
  5. [5]
    A. Ehrenfeucht and G. Rozenberg: Partial 2-structures; Part II, State spaces of concurrent systems, Acta Inf. 27 (1990) 348–368.Google Scholar
  6. [6]
    J.G. Henriksen, M. Mukund, K. Narayan Kumar and P.S. Thiagarajan: Regular Collections of Message Sequence Charts, Proc. MFCS 2000, LNCS 1893 (2000), 405–414.MathSciNetGoogle Scholar
  7. [7]
    G.J. Holzmann: The model checker SPIN, IEEE Trans. on Software Engineering, 23, 5 (1997) 279–295.Google Scholar
  8. [8]
    R.P. Kurshan: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press (1994).Google Scholar
  9. [9]
    A. Mazurkiewicz: Basic notions of trace theory, in: J.W. de Bakker, W.-P. de Roever, G. Rozenberg (eds.), Linear time, branching time and partial order in logics and models for concurrency, LNCS, 354 (1989) 285–363.Google Scholar
  10. [10]
    R. Milner: Communication and Concurrency, Prentice-Hall, London (1989).zbMATHGoogle Scholar
  11. [I1]
    R. Morin: Decompositions of asynchronous systems, Proc. CONCUR’98, LNCS 1466 (1998) 549–564.MathSciNetGoogle Scholar
  12. [12]
    M. Mukund: Petri Nets and Step Transition Systems, Int. J. Found. Comput. Sci. 3, 4 (1992) 443–478.Google Scholar
  13. [ 13]
    M. Mukund, K. Narayan Kumar, M. Sohoni: Synthesizing distributed finite-state systems from MSCs, Proc. CONCUR 2000, LNCS 1877 (2000) 521–535.MathSciNetGoogle Scholar
  14. [14]
    M. Mukund, M. Sohoni: Gossiping, asynchronous automata and Zielonka’s theorem, Report TCS-94–2,Chennai Mathematical Institute (1994). Available via
  15. [15]
    M. Nielsen, G. Rozenberg and P.S. Thiagarajan: Elementary transition systems, Theor. Comput. Sci. 96 (1992) 3–33.MathSciNetzbMATHCrossRefGoogle Scholar
  16. [ 16]
    P.S. Thiagarajan: A trace consistent subset of PTL, Proc. CONCUR’95, LNCS 962 (1995) 438–452.Google Scholar
  17. [17]
    G. Winskel and M. Nielsen: Models for concurrency, in S. Abramsky, D. Gabbay and T.S.E. Maibaum, eds, Handbook of Logic in Computer Science, Vol 4, Oxford (1995) 1–148.Google Scholar
  18. [18]
    W. Zielonka: Notes on finite asynchronous automata, R.A.LR.O.—Inform. Théor. Appl.,21(1987)99–135.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2002

Authors and Affiliations

  • Madhavan Mukund
    • 1
  1. 1.Chennai Mathematical InstituteChennaiItaly

Personalised recommendations