J G Henriksen, M Mukund, K Narayan Kumar and P S Thiagarajan
Proc. ICALP '00, Springer LNCS 1853 (2000) 675-686.
© Springer-Verlag Berlin Heidelberg
Message Sequence Charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the early design stages in domains such as telecommunication software. A standard method to describe multiple communication scenarios is to use message sequence graphs (MSGs). A message sequence graph allows the protocol designer to write a finite specification which combines MSCs using basic operations such as branching choice, composition and iteration. The MSC languages described by MSGs are not necessarily regular in the sense of [HM+99]. We characterize here the class of regular MSC languages that are MSG-definable in terms of a notion called finitely generated MSC languages. We show that a regular MSC language is MSG-definable if and only if it is finitely generated. In fact we show that the subclass of ``bounded'' MSGs defined in [AY99] exactly capture the class of finitely generated regular MSC languages.