Skip to main content
SpringerLink
Log in

The Pros and Cons of Netcharts

  • Conference paper
Book cover CONCUR 2004 - Concurrency Theory (CONCUR 2004)

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

Included in the following conference series:

Abstract

Netcharts have been introduced recently by Mukund et al. in [17]. This new appealing approach to the specification of collections of message sequence charts (MSCs) benefits from a graphical description, a formal semantics based on Petri nets, and an appropriate expressive power. As opposed to high-level MSCs, any regular MSC language is the language of some netchart. Motivated by two open problems raised in [17], we establish in this paper that the questions

(i) whether a given high-level MSC describes some netchart language

(ii) whether a given netchart is equivalent to some high-level MSC

(iii) whether a given netchart describes a regular MSC language

are undecidable. These facts are closely related to our first positive result: We prove that netchart languages are exactly the MSC languages that are implementable by message passing automata up to refinement of message contents. Next we focus on FIFO netcharts: The latter are defined as the netcharts whose executions correspond to all firing sequences of their low-level Petri net. We show that the questions

(i) whether a netchart is a FIFO netchart

(ii) whether a FIFO netchart describes a regular MSC language

(iii) whether a regular netchart is equivalent to some high-level MSC

are decidable.

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. Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 797–808. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  2. Alur, R., Yannakakis, M.: Model Checking of Message Sequence Charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Baudru, N., Morin, R.: Safe Implementability of Regular Message Sequence Charts Specifications. In: Proc. of the ACIS 4th Int. Conf. SNDP 2003, pp. 210–217 (2003)

    Google Scholar 

  4. Bollig, B., Leucker, M., Noll, T.G.: Generalised Regular MSC Languages. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 52–66. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Caillaud, B., Darondeau, P., Hélouët, L., Lesventes, G.: HMSCs as Partial Specifications. with PNs as Completions. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 87–103. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific, Singapore (1995)

    Book  Google Scholar 

  7. Gunter, E.L., Muscholl, A., Peled, D.A.: Compositional Message Sequence Charts. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 496–511. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: On Message Sequence Graphs and Finitely Generated Regular MSC Languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 675–686. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: Regular Collections of Message Sequence Charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 405–414. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Holzmann, G.J.: Early Fault Detection. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 1–13. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  11. ITU-TS Recommendation Z.120: Message Sequence Charts (1996) (Geneva)

    Google Scholar 

  12. Lambert, J.L.: A structure to decide reachability in Petri nets. Theoretical Comp. Science 99, 79–104 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  13. Lamport, L.: Time, Clocks and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  14. Lohrey, M.: Realizability of High-level Message Sequence Charts: closing the gaps. Theoretical Comp. Science 309, 529–554 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  15. Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM Journal of Computing 13(3), 441–460 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  16. Morin, R.: Recognizable Sets of Message Sequence Charts. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 523–534. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: Netcharts: Bridging the Gap between HMSCs and Executable Specifications. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 296–310. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 81–91. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Muscholl, A., Peled, D.A.: From Finite State Communication Protocols to High-Level Message Sequence Charts. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 720–731. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  20. Pratt, V.: Modelling concurrency with partial orders. International Journal of Parallel Programming 15, 33–71 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  21. Wimmel, H.: Infinity of Intermediate States is Decidable for Petri Nets Applications and Theory of Petri Nets, LNCS (to appear, 2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique Fondamentale de Marseille, Université de Provence, 39 rue F. Joliot-Curie, F-13453 cedex 13, Marseille, France

    Nicolas Baudru & Rémi Morin

Authors
  1. Nicolas Baudru
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rémi Morin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2AZ, London, UK

    Philippa Gardner

  2. Department of Computing, Imperial College, London, UK

    Nobuko Yoshida

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baudru, N., Morin, R. (2004). The Pros and Cons of Netcharts. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-28644-8_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22940-7

  • Online ISBN: 978-3-540-28644-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation