Skip to main content
SpringerLink
Log in
Book cover

International Computer Science Symposium in Russia

CSR 2010: Computer Science – Theory and Applications pp 48–59Cite as

Realizability of Dynamic MSC Languages

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6072))

Abstract

We introduce dynamic communicating automata (DCA), an extension of communicating finite-state machines that allows for dynamic creation of processes. Their behavior can be described as sets of message sequence charts (MSCs). We consider the realizability problem for DCA: given a dynamic MSC grammar (a high-level MSC specification), is there a DCA defining the same set of MSCs? We show that this problem is decidable in doubly exponential time, and identify a class of realizable grammars that can be implemented by finite DCA.

Partly supported by the projects ANR-06-SETI-003 DOTS and ARCUS Île de France-Inde.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Adsul, B., Mukund, M., Narayan Kumar, K., Narayanan, V.: Causal closure for MSC languages. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 335–347. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. Theoretical Computer Science 331(1), 97–114 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bollig, B., Hélouët, L.: Realizability of dynamic MSC languages. Research report, LSV, ENS Cachan (2010), http://www.lsv.ens-cachan.fr/Publis/

  4. Bozzelli, L., La Torre, S., Peron, A.: Verification of well-formed communicating recursive state machines. Theoretical Computer Science 403(2-3), 382–405 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  5. Brand, D., Zafiropulo, P.: On communicating finite-state machines. JACM 30(2) (1983)

    Google Scholar 

  6. Gazagnaire, T., Genest, B., Hélouët, L., Thiagarajan, P.S., Yang, S.: Causal message sequence charts. Theor. Comput. Sci. 410(41), 4094–4110 (2009)

    Article  MATH  Google Scholar 

  7. Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state high-level MSCs: Model-checking and realizability. Journal on Comp. and System Sciences 72(4), 617–647 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  8. Gunter, E.L., Muscholl, A., Peled, D.: Compositional message sequence charts. STTT 5(1), 78–89 (2003)

    Google Scholar 

  9. Hélouët, L., Jard, C.: Conditions for synthesis of communicating automata from HMSCs. In: FMICS’00, pp. 203–224. Springer, Heidelberg (2000)

    Google Scholar 

  10. Henriksen, J.G., Mukund, M., Narayan Kumar, K., Sohoni, M., Thiagarajan, P.S.: A theory of regular MSC languages. Information and Computation 202(1), 1–38 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  11. Leucker, M., Madhusudan, P., Mukhopadhyay, S.: Dynamic message sequence charts. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 253–264. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theoretical Computer Science 309(1-3), 529–554 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  13. Rudolph, E., Graubmann, P., Grabowski, J.: Tutorial on message sequence charts. Computer Networks and ISDN Systems 28(12), 1629–1641 (1996)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan, CNRS, INRIA, France

    Benedikt Bollig

  2. IRISA, INRIA, Rennes, France

    Loïc Hélouët

Authors
  1. Benedikt Bollig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Loïc Hélouët
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Theoretical Cybernetics, Kazan State University, 420008, Kazan, Russia

    Farid Ablayev

  2. Institut für Informatik, Technische Universität München, 85748, Garching, Germany

    Ernst W. Mayr

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bollig, B., Hélouët, L. (2010). Realizability of Dynamic MSC Languages. In: Ablayev, F., Mayr, E.W. (eds) Computer Science – Theory and Applications. CSR 2010. Lecture Notes in Computer Science, vol 6072. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13182-0_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13182-0_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13181-3

  • Online ISBN: 978-3-642-13182-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation