Advertisement

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. AEY00.
    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. AY99.
    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. GMP01.
    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. HMKT99.
    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. HMKT00a.
    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. HMKT00b.
    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. Mad01.
    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. MM01.
    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. MR00.
    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. Pel00.
    D. Peled. Specification and verification of message sequence charts. In Proc. IFIP FORTE/PSTV, 2000.Google Scholar
  11. RGG96.
    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. Tho90.
    W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 165–191, 1990.Google Scholar
  13. Tho97.
    W. Thomas. Languages, automata, and logic. Handbook of Formal Language Theory, III:389–455, 1997.Google Scholar
  14. TW97.
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • P. Madhusudan
    • 1
  • B. Meenakshi
    • 2
  1. 1.Chennai Mathematical InstituteChennaiIndia
  2. 2.The Institute of Mathematical SciencesChennaiIndia

Personalised recommendations