Regular Collections of Message Sequence Charts

Extended Abstract
  • Jesper G. Henriksen
  • Madhavan Mukund
  • K. Narayan Kumar
  • P. S. Thiagarajan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)


Message Sequence Charts (MSCs) are an attractive visual formalism used during the early stages of design in domains such as telecommunication software. A popular mechanism for generating a collection of MSCs is a Hierarchical Message Sequence Chart (HMSC). However, not all HMSCs describe collections of MSCs that can be “realized” as a finite-state device. Our main goal is to pin down this notion of realizability. We propose an independent notion of regularity for collections of MSCs and explore its basic properties. In particular, we characterize regular collections of MSCs in terms of finite-state distributed automata called bounded message-passing automata, in which a set of sequential processes communicate with each other asynchronously over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. It turns out that realizable collections of MSCs as specified by HMSCs constitute a strict subclass of the regular collections of MSCs.


Message Sequence Chart Logical Characterization Regular Subset Asynchronous Automaton Regular Collection 
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.
    Alur, R., Holzmann, G. J., and Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools, 17(2) (1996) 70–77.zbMATHGoogle Scholar
  2. 2.
    Alur, R., and Yannakakis, M.: Model checking of message sequence charts. Proc. CONCUR’99, LNCS 1664, Springer-Verlag (1999) 114–129.Google Scholar
  3. 3.
    Ben-Abdallah, H., and Leue, S.: Syntactic detection of process divergence and nonlocal choice in message sequence charts. Proc. TACAS’97, LNCS 1217, Springer-Verlag (1997) 259–274.Google Scholar
  4. 4.
    Booch, G., Jacobson, I., and Rumbaugh, J.: Unified Modeling Language User Guide. Addison-Wesley (1997).Google Scholar
  5. 5.
    Büchi, J. R.: On a decision method in restricted second order arithmetic. Z. Math. Logik Grundlag. Math 6 (1960) 66–92.zbMATHCrossRefGoogle Scholar
  6. 6.
    Damm, W., and Harel, D.: LCSs: Breathing life into message sequence charts. Proc. FMOODS’99, Kluwer Academic Publishers (1999) 293–312.Google Scholar
  7. 7.
    Diekert, V., and Rozenberg, G. (Eds.): The book of traces. World Scientific (1995).Google Scholar
  8. 8.
    Ebinger, W., and Muscholl, A.: Logical definability on infinite traces. Theoretical Computer Science 154(1) (1996) 67–84.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Harel, D., and Gery, E.: Executable object modeling with statecharts. IEEE Computer, July 1997 (1997) 31–42.Google Scholar
  10. 10.
    Henriksen, J. G., Mukund, M., Narayan Kumar, K., and Thiagarajan, P. S.: Towards a theory of regular MSC languages, Report RS-99-52, BRICS, Department of Computer Science, University of Aarhus, Denmark (1999).Google Scholar
  11. 11.
    Henriksen, J. G., Mukund, M., Narayan Kumar, K., and Thiagarajan, P. S.: On message sequence graphs and finitely generated regular MSC languages, Proc. ICALP’2000, LNCS 1853, Springer-Verlag (2000).Google Scholar
  12. 12.
    ITU-TS Recommendation Z. 120: Message Sequence Chart (MSC). ITU-TS, Geneva (1997)Google Scholar
  13. 13.
    Ladkin, P. B., and Leue, S.: Interpreting message flow graphs. Formal Aspects of Computing 7(5) (1995) 473–509.zbMATHCrossRefGoogle Scholar
  14. 14.
    Levin, V., and Peled, D.: Verification of message sequence charts via template matching. Proc. TAPSOFT’97, LNCS 1214, Springer-Verlag (1997) 652–666.Google Scholar
  15. 15.
    Mauw, S., and Reniers, M. A.: High-level message sequence charts, Proc. SDL’ 97, Elsevier (1997) 291–306.Google Scholar
  16. 16.
    Mukund, M., Narayan Kumar, K., and Sohoni, M.: Keeping track of the latest gossip in message-passing systems. Proc. Structures in Concurrency Theory (STRICT), Workshops in Computing Series, Springer-Verlag (1995) 249–263.Google Scholar
  17. 17.
    Muscholl, A.: Matching Specifications for Message Sequence Charts. Proc. FOSSACS’99, LNCS 1578, Springer-Verlag (1999) 273–287.Google Scholar
  18. 18.
    Muscholl, A., Peled, D., and Su, Z.: Deciding properties for message sequence charts. Proc. FOSSACS’98, LNCS 1378, Springer-Verlag (1998) 226–242.Google Scholar
  19. 19.
    Rudolph, E., Graubmann, P., and Grabowski, J.: Tutorial on message sequence charts. In Computer Networks and ISDN Systems—SDL and MSC, Volume 28 (1996).Google Scholar
  20. 20.
    Thiagarajan, P. S., and Walukiewicz, I: An expressively complete linear time temporal logic for Mazurkiewicz traces. Proc. IEEE LICS’97 (1997) 183–194.Google Scholar
  21. 21.
    Thomas, W.: Automata on infinite objects. In van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science, Volume B, North-Holland (1990) 133–191.Google Scholar
  22. 22.
    Vardi, M. Y., and Wolper, P.: An automata-theoretic approach to automatic program verification. In Proc. IEEE LICS’86 (1986) 332–344.Google Scholar
  23. 23.
    Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O.—Inf. Théor. et Appl., 21 (1987) 99–135.MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Jesper G. Henriksen
    • 1
  • Madhavan Mukund
    • 2
  • K. Narayan Kumar
    • 2
  • P. S. Thiagarajan
    • 2
  1. 1.BRICSUniversity of AarhusDenmark
  2. 2.Chennai Mathematical InstituteChennaiIndia

Personalised recommendations