Pattern matching and membership for hierarchical message sequence charts

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.