Skip to main content
SpringerLink
Log in

Extending Compositional Message Sequence Graphs

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2514))

Abstract

We extend the formal developments for message sequence charts (MSCs) to support scenarios with lost and found messages. We define a notion of extended compositional message sequence charts (ECM-SCs) which subsumes the notion of compositional message sequence charts in expressive power but additionally allows to define lost and found messages explicitly. As usual, ECMSCs can be combined by means of choice and repetition to (extended) compositional message sequence graphs. We show that—despite extended expressive power—model checking of monadic second-order logic (MSO) for this framework remains to be decidable. The key technique to achieve our results is to use an extended notion for linearizations.

Part of this work was done during the author’s stay at the IT department, Uppsala University, Sweden. He is grateful for the hospitality and the overall support.

The research was mainly accomplished during the author’s stay at Dept. of Computer and Information Science, University of Pennsylvania, USA, and was supported in part by NSF CCR-9988409, NSF CCR-0086147, NSF CISE-9703220, ARO DAAD19-01-1-0473, DARPA ITO MOBIES F33615-00-C-1707, and ONR N00014-97-1-0505. Additionally, the work was supported by the European Research Training Network on “Games”, HPRN-CT-2002-00283.

supported in part by “Graduiertenkolleg Leistungsgarantien für Rechnersysteme”

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 and M. Yannakakis. Model checking of message sequence charts. In Proc. of the 10th International Conference on Concurrency Theory, LNCS 1664, pp. 114–129. Springer, 1999.

    Google Scholar 

  2. J. Araújo. Formalizing sequence diagrams. In L. Andrade, A. Moreira, A. Deshpande, and S. Kent, editors, Proc. of the OOPSLA’ 98 Workshop on Formalizing UML. Why? How?, volume 33, 10 of A CM SIGPLAN Notices, New York, 1998. ACM Press.

    Google Scholar 

  3. B. Bollig and M. Leucker. Deciding LTL over Mazurkiewicz traces. In C. Bettini and A. Montanari, editors, Proc. of the Symposium on Temporal Representation and Reasoning (TIME’01), pp. 189–197. IEEE Computer Society Press, 2001.

    Google Scholar 

  4. B. Bollig and M. Leucker. Modelling, Specifying, and Verifying Message Passing Systems. In C. Bettini and A. Montanari, editors, Proc. of the Symposium on Temporal Representation and Reasoning (TIME’01), pp. 240–248. IEEE Computer Society Press, 2001.

    Google Scholar 

  5. B. Bollig, M. Leucker, and P. Lucas. Extending compositional message sequence graphs. Technical Report MS-CIS-02-09, University of Pennsylvania, Apr. 2002.

    Google Scholar 

  6. B. Bollig, M. Leucker, and T. Noll. Generalised regular MSC languages. In Proc. of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’ 02), LNCS 2303, pp. 52–66. Springer, 2002.

    Chapter  Google Scholar 

  7. W. Damm and D. Harel. LSC’s: Breathing life into message sequence charts. Technical Report CS98-09, Weizmann Institute of Science, Apr. 1998.

    Google Scholar 

  8. V. Diekert and Y. Métivier. Partial commutation and traces. In G. Rozenberg and A. Salomaa, editors, Handbook on Formal Languages, volume III. Springer, 1997.

    Google Scholar 

  9. E. Gunter, A. Muscholl, and D. Peled. Compositional message sequence charts. In T. Margaria and W. Yi, editors, Proc. of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), LNCS 2031. Springer, Apr. 2001.

    Chapter  Google Scholar 

  10. J. G. Henriksen, M. Mukund, K. N. Kumar, and P. S. Thiagarajan. On message sequence graphs and finitely generated regular msc languages. In Proc. of 27th International Colloquium on Automata, Languages and Programming (ICALP’2000), LNCS 1853, pp. 675–686. Springer, 2000.

    Chapter  Google Scholar 

  11. J. G. Henriksen, M. Mukund, K. N. Kumar, and P. S. Thiagarajan. Regular collections of message sequence charts. In Proc. of 25th International Symposium on Mathematical Foundations of Computer Science (MFCS’2000), LNCS 1893, pp. 405–414. Springer, 2000.

    Google Scholar 

  12. ITU-TS. ITU-TS Recommendation Z.120anb: Formal Semantics of Message Sequence Charts. Technical report, ITU-TS, Geneva, 1998.

    Google Scholar 

  13. ITU-TS. ITU-TS Recommendation Z.120: Message Sequence Chart 1999 (MSC99). Technical report, ITU-TS, Geneva, 1999.

    Google Scholar 

  14. D. Kuske. Another step towards a theory of regular MSC languages. In Proc. of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS’02), LNCS 2285. Springer, 2002.

    Google Scholar 

  15. P. Madhusudan. Reasoning about sequential and branching behaviours of message sequence graphs. In Proc. of 27th International Colloquium on Automata, Languages and Programming (ICALP’2000), LNCS 2076. Springer, 2001.

    Google Scholar 

  16. P. Madhusudan and B. Meenakshi. Beyond message sequence graphs. In Proc. of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 2245, pp. 256–267. Springer, 2001.

    Google Scholar 

  17. S. Mauw and M. A. Reniers. High-level message sequence charts. In Proc. of the Eighth SDL Forum (SDL’97), pp. 291–306, 1997.

    Google Scholar 

  18. B. Meenakshi and R. Ramanujam. Reasoning about message passing in finite state environments. In F. Orejas, P. G. Spirakis, and J. van Leeuwen, editors, Proc. of 27th International Colloquium on Automata, Languages and Programming (ICALP’2000), LNCS 1853. Springer, 2000.

    Chapter  Google Scholar 

  19. R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

    Google Scholar 

  20. R. Morin. Recognizable sets of message sequence charts. In Proc. of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS’02), 2002, LNCS 2285. Springer, 2002.

    Google Scholar 

  21. D. Peled. Specification and verification of message sequence charts. In Proc. IFIP FORTE/PSTV, pp. 139–154, 2000.

    Google Scholar 

  22. P. S. Thiagarajan. A trace consistent subset of PTL. In I. Lee and S. A. Smolka, editors, Proc. of the 6th International Conference on Concurrency Theory (CONCUR’95), LNCS 962, pp. 438–452, Philadelphia, Pennsylvania, 1995. Springer.

    Google Scholar 

  23. P. S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. In Proc. 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, 1997. IEEE Computer Society Press.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lehrstuhl für Informatik II, RWTH Aachen, Germany

    Benedikt Bollig & Philipp Lucas

  2. Department of Computer Systems, Uppsala University, Sweden

    Martin Leucker

  3. Universität des Saarlandes, Saarbrücken, Germany

    Philipp Lucas

Authors
  1. Benedikt Bollig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Leucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Philipp Lucas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria

    Matthias Baaz

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, M13, 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bollig, B., Leucker, M., Lucas, P. (2002). Extending Compositional Message Sequence Graphs. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-36078-6_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-36078-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation