Abstract
We introduce a formalism to specify classes of MSCs over an unbounded number of processes. The formalism can describe many interesting behaviours of dynamically changing networks of processes. Moreover, it strictly includes the formalism of Message Sequence Graphs studied in the literature to describe MSCs over a fixed finite set of processes. Our main result is that model-checking of MSCs described in this formalism against a suitable monadic-second order logic is decidable.
supported by DARPA MOBIES F33615-00-C-1707, NSF CCR-9988409, NSF CISE- 9703220, and the European Research Training Network on “Games”
supported by NSF awards CCR99-70925 and ITR/SY 0121431
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
R. Alur and M. Yannakakis. Model checking of message sequence charts. In Proc. 10th Int’l. Conf. on Concurrency Theory, LNCS 1664, p. 114–129. Springer, 1999.
D. Caucal. On infinite transition graphs having a decidable monadic theory. In Proc. the 23th International Colloquium on Automata, Languages and Programming (ICALP’96), LNCS 1099, p. 194–205, Springer, 1996.
B. Courcelle. On the expression of graph properties in some fragments of monadic second-order logic. In Descriptive complexity and finite models, volume 31. DIMACS Series in Discrete Mathematics and Theoretical Computer Sciences, June 1997.
M. Leucker, P. Madhusudan, and S. Mukhopadhyay. Dynamic message sequence charts. Technical Report MS-CIS-02-27, University of Pennsylvania, 2002.
P. Madhusudan. Reasoning about sequential and branching behaviours of message sequence graphs. In Proc. 27th International Colloquium on Automata, Languages and Programming (ICALP’01), LNCS 2076, p. 396–407. Springer, 2001.
P. Madhusudan and B. Meenakshi. Beyond message sequence graphs. In Proc. 21st Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 2245, p. 256–267. Springer, 2001.
R. Milner. A Calculus for Communicating Processes, LNCS 92, Springer, 1980.
ITU-TS. ITU-TS Recommendation Z.120: Message Sequence Chart 1996 (MSC96). Technical report, ITU-TS, Geneva, 1996.
W. Thomas. Languages, automata and logic. In Handbook of Formal Languages, volume 3, Beyond Words. Springer, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leucker, M., Madhusudan, P., Mukhopadhyay, S. (2002). Dynamic Message Sequence Charts. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_23
Download citation
DOI: https://doi.org/10.1007/3-540-36206-1_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00225-3
Online ISBN: 978-3-540-36206-7
eBook Packages: Springer Book Archive