Abstract
Message sequence charts (MSC) are a graphical specification language widely used for designing communication protocols. Our starting point are two decision problems concerning the correctness and the consistency of a design based by MSC graphs. Both problems are shown to be undecidable, in general. Using a natural connectivity assumption from Mazurkiewicz trace theory we show both problems to be EXPSPACE-complete for locally synchronized graphs. The results are based on new complexity results for star-connected rational trace languages.
The results were partly supported by Bell Labs and DIMACS.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. Alur, G. H. Holzmann, and D. A. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70–77, 1996.
H. Ben-Abdallah and S. Leue. Syntactic detection of process divergence and non local choice in message sequence charts. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), LNCS 1217, pp. 259–274.
M. Clerbout. Commutations Partielles et Families de Langages. Thèse, Université des Sciences et Technologies de Lille (France), 1984.
M. Clerbout and M. Latteux. Semi-Commutations. Information and Computation, 73:59–74, 1987.
V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.
S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2):285–296, 1966.
G. Holzmann, D. Peled, and M. Redberg. Design tools for requirements engineering. Bell Labs Technical Journal-Software, 2(1):86–95, 1997.
A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.
Y. Métivier. Une condition suffisante de reconnaissabilité dans un monoïde partiellement commutatif. R.A.I.R.O. — Informatique Théorique et Applications, 20:121–127, 1986.
Y. Métivier. On recognizable subsets of free partially comutative monoids. Theoretical Computer Science, 58:201–208, 1988.
A. Muscholl. Decision and complexity issues on concurrent systems. Habilitationsschrift (postdoctoral thesis), Universität Stuttgart, Jan. 1999. Submitted.
A. Muscholl, D. Peled, and Z. Su. Deciding properties of message sequence charts. In Proc. of the 1st Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS’98), LNCS 1378, pp. 226–242, 1998.
E. Ochmański. Regular behaviour of concurrent systems. Bulletin of the European Association for Theoretical Computer Science (EATCS), 27:56–67, Oct. 1985.
J. Sakarovitch. The “last” decision problem for rational trace languages. Report LITP 91.77, Univ. Paris 6, 1991. Abstract presented at the 1st Int. Symp. of Latin American Theor. Informatics (LATIN’92), LNCS 583 (1992), pp. 460–473.
I. Walukiewicz. Difficult configurations — on the complexity of LTrL. In Proc. of the 25th International Colloquium on Automata, Languages and Programming (ICALP’98), LNCS 1443, pp. 140–151, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Muscholl, A., Peled, D. (1999). Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces. In: Kutyłowski, M., Pacholski, L., Wierzbicki, T. (eds) Mathematical Foundations of Computer Science 1999. MFCS 1999. Lecture Notes in Computer Science, vol 1672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48340-3_8
Download citation
DOI: https://doi.org/10.1007/3-540-48340-3_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66408-6
Online ISBN: 978-3-540-48340-3
eBook Packages: Springer Book Archive