Abstract
Several formalisms and tools for software development use hierarchy for system design, for instance statecharts and diagrams in UML. Message sequence charts are an ITU standardized notation for asynchronously communicating processes. The standard Z.120 allows (high-level) MSC-references that correspond to the use of macros. We consider in this paper two basic verification tasks for hierarchical MSCs (nested high-level MSCs, nHMSC), the membership and the pattern matching problem. We show that the membership problem for nHMSCs is PSPACE-complete, even using a weaker semantics for nMSCs than the partial-order semantics. For pattern matching nMSCs M,N we exhibit a polynomial algorithm of time O(M 2 · N 2). We use here techniques stemming from algorithms on compressed texts.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification of MSC graphs. In ICALP’01, LNCS 2076, pp. 797–808, 2001.
R. Alur, G. H. Holzmann, and D. A. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70–77, 1996.
R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In ICALP’99, LNCS 1644, pp. 169–178, 1999.
R. Alur and M. Yannakakis. Model checking of hierarchical state machines. In SIGSOFT’ 98, pp. 175–188, 1998.
R. Alur and M. Yannakakis. Model checking of message sequence charts. In CONCUR’99, LNCS 1664, pp. 114–129, 1999.
N.J. Fine and H.S. Wilf. Uniqueness theorems for periodic functions. Proceedings of the American Mathematical Society, 16, 1965.
E. Gunter, A. Muscholl, and D. Peled. Compositional message sequence charts. In TACAS’01, LNCS 2031, pp. 496–511, 2001.
D. Harel. Statecharts: A visual formulation for complex systems. Science of Computer Programming, 8(3):231–274, 1987.
M. Y. Vardi, D. Harel, O. Kupferman. On the complexity of verifying concurrent transition systems. In CONCUR’ 97, LNCS 1243, pp. 258–272, 1997.
P. Madhusudan. Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs. In ICALP’01, LNCS 2076, pp. 809–820, 2001.
A. Muscholl and D. Peled. Message sequence graphs and decision problems on Mazurkiewicz traces. In MFCS’99, LNCS 1672, pp. 81–91, 1999.
A. Muscholl, D. Peled, and Z. Su. Deciding properties of message sequence charts. In FoSSaCS’98, LNCS 1378, pp. 226–242, 1998.
M. Miyazaki, A. Shinohara, and M. Takeda. An improved pattern matching algorithm for strings in terms of straight-line programs. In CPM’ 97, LNCS 1264.
W. Plandowski. Testing equivalence of morphisms on context-free languages. In ESA’ 94, pp. 460–470, 1994.
W. Rytter. Algorithms on compressed strings and arrays. In SOFSEM’ 99, LNCS 1725, pp. 48–65, 1999.
T. J. Schaefer. The complexity of satisfiability problems. In STOC’ 78, pp. 216–226, 1978.
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
Genest, B., Muscholl, A. (2002). Pattern Matching and Membership for Hierarchical Message Sequence Charts. In: Rajsbaum, S. (eds) LATIN 2002: Theoretical Informatics. LATIN 2002. Lecture Notes in Computer Science, vol 2286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45995-2_31
Download citation
DOI: https://doi.org/10.1007/3-540-45995-2_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43400-9
Online ISBN: 978-3-540-45995-8
eBook Packages: Springer Book Archive