Skip to main content
SpringerLink
Log in

Beyond Message Sequence Graphs

  • Conference paper
  • First Online:
FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2245))

Abstract

We study the model-checking problem for classes of message sequence charts (MSCs) defined by two extensions of message sequence graphs (MSGs). These classes subsume the class of regular MSC languages. We show that the model checking problem for these extended message sequence graphs against monadic second-order specifications is decidable. Moreover, we present two ways to model-check the extended classes — one extends the proof for MSGs while the other extends the proof for regular MSC languages.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts. In Proc. 22nd Intl. Conf. on Software Engg., pages 304–313, 2000.

    Google Scholar 

  2. R. Alur and M. Yannakakis. Model checking of message sequence charts. In Proc. CONCUR’ 99, vol. 1664 of LNCS. Springer-Verlag, 1999.

    Google Scholar 

  3. E. Gunter, A. Muscholl, and D. Peled. Compositional message sequence charts. In Proc. TACAS’01, vol. 2031 of LNCS, pages 496–511. Springer-Verlag, 2001.

    Google Scholar 

  4. J.G. Henriksen, M. Mukund, Narayan Kumar, and P.S. Thiagarajan. Towards a theory of regular MSC languages. BRICS Report RS-99-52, Department of Computer Science, Aarhus University, Denmark, 1999.

    Google Scholar 

  5. J.G. Henriksen, M. Mukund, Narayan Kumar, and P.S. Thiagarajan. On message sequence graphs and finitely generated regular MSC languages. In Proc. ICALP’ 00, vol. 1853 of LNCS. Springer-Verlag, 2000.

    Google Scholar 

  6. J.G. Henriksen, M. Mukund, Narayan Kumar, and P.S. Thiagarajan. Regular collections of Message Sequence Charts. In Proc. MFCS’ 00, vol. 1893 of LNCS. Springer-Verlag, 2000.

    Google Scholar 

  7. P. Madhusudan. Reasoning about sequential and branching behaviours of message sequence graphs. In Proc. ICALP’ 01, vol. 2076 of LNCS. Springer-Verlag, 2001.

    Google Scholar 

  8. P. Madhusudan, B. Meenakshi. Beyond Message Sequence Graphs. Institute of Mathematical Sciences Technical Report, IMSc./2001/09/51. Available at http://www.imsc.ernet.in/~madhuor/~bmeena.

  9. B. Meenakshi and R. Ramanujam. Reasoning about message passing in finite state environments. In Proc. ICALP’ 00, vol. 1853 of LNCS. Springer-Verlag, 2000.

    Google Scholar 

  10. D. Peled. Specification and verification of message sequence charts. In Proc. IFIP FORTE/PSTV, 2000.

    Google Scholar 

  11. E. Rudolph, P. Graubmann, and J. Grabowski. Tutorial on message sequence charts. In Computer Networks and ISDN Systems-SDL and MSC, Vol. 28, 1996.

    Google Scholar 

  12. W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 165–191, 1990.

    Google Scholar 

  13. W. Thomas. Languages, automata, and logic. Handbook of Formal Language Theory, III:389–455, 1997.

    Google Scholar 

  14. P.S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. In Proc. 12th IEEE Conf. on Logic in Computer Science. IEEE Computer Society, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Chennai Mathematical Institute, Chennai, India

    P. Madhusudan

  2. The Institute of Mathematical Sciences, Chennai, India

    B. Meenakshi

Authors
  1. P. Madhusudan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. B. Meenakshi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Automation, Indian Institute of Science, 560012, Bangalore, India

    Ramesh Hariharan  & V. Vinay  & 

  2. Chennai Mathematical Institute, 92 G.N. Chetty Road, 600 017, Chennai, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Madhusudan, P., Meenakshi, B. (2001). Beyond Message Sequence Graphs. In: Hariharan, R., Vinay, V., Mukund, M. (eds) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2001. Lecture Notes in Computer Science, vol 2245. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45294-X_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-45294-X_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43002-5

  • Online ISBN: 978-3-540-45294-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation