Abstract
Scenario languages based on Message Sequence Charts (MSCs) and related notations have been widely studied in the last decade [14,13,2,9,6,12,8]. The high expressive power of scenarios renders many basic problems concerning these languages undecidable. The most expressive class for which several problems are known to be decidable is one which possesses a behavioral property called “existentially bounded”. However, scenarios outside this class are frequently exhibited by asynchronous distributed systems such as sliding window protocols. We propose here an extension of MSCs called Causal Message Sequence Charts, which preserves decidability without requiring existential bounds. Interestingly, it can also model scenarios from sliding window protocols. We establish the expressive power and complexity of decision procedures for various subclasses of Causal Message Sequence Charts.
Work supported by the INRIA-NUS Associated Team CASDS and the ANR projects DOTS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahuja, M., Kshemkalyani, A.D., Carlson, T.: A basic unit of computation in distributed sytems. In: Proc. of ICDS 1990, pp. 12–19 (1990)
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)
Brand, D., Zafiropoulo, P.: On communicating finite state machines. Technical Report RZ1053, IBM Zurich Research Lab (1981)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking for a class of communicating automata. Information and Computation 204(6), 920–956 (2006)
Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state high-level MSCs: Model-checking and realizability. Journal of Computer and System Sciences 72(4), 617–647 (2006)
Gunter, E., Muscholl, A., Peled, D.: Compositional message sequence charts. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, Springer, Heidelberg (2001)
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)
Hélouët, L., Le Maigat, P.: Decomposition of message sequence charts. In: Proc. of SAM 2000 (2000)
ITU-TS: ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS (1999)
Kuske, D.: Regular sets of infinite message sequence charts. Information and Computation 187(1), 80–109 (2003)
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)
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, Springer, Heidelberg (1999)
Muscholl, A., Peled, D., Su, Z.: Deciding properties for message sequence charts. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, pp. 226–242. Springer, Heidelberg (1998)
Reniers, M.: Message Sequence Chart: Syntax and Semantics. PhD thesis, Eindhoven University of Technology (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gazagnaire, T., Genest, B., Hélouët, L., Thiagarajan, P.S., Yang, S. (2007). Causal Message Sequence Charts. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)