Madhavan Mukund

Synthesizing distributed finite-state systems from MSCs

M Mukund, K Narayan Kumar and M Sohoni

Proc. CONCUR '00, Springer LNCS 1877 (2000) 521-535.

© Springer-Verlag Berlin Heidelberg


Message sequence charts (MSCs) are an appealing visual formalism often used to capture system requirements in the early stages of design. An important question concerning MSCs is the following: how does one convert requirements represented by MSCs into state-based specifications? A first step in this direction was the definition in [Henriksen et al, MFCS 2000] of regular collections of MSCs, together with a characterization of this class in terms of finite-state distributed devices called message-passing automata. These automata are, in general, nondeterministic. In this paper, we strengthen this connection and describe how to directly associate a deterministic message-passing automaton with each regular collection of MSCs. Since real life distributed protocols are deterministic, our result is a more comprehensive solution to the synthesis problem for MSCs. Our result can be viewed as an extension of Zielonka's theorem for Mazurkiewicz trace languages [DiekertRozenberg1995, Zielonka1987] to the setting of finite-state message-passing systems.

  • Download PDF.