Towards a Theory of Regular MSC Languages

Message Sequence Charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the earlydesign stages in domains such as telecommunication software. It isfruitful to have mechanisms for specifying and reasoning about collections of MSCs so that errors can be detected even at the requirements level. We propose, accordingly, a notion of regularity for collections of MSCs and explore its basic properties. In particular, weprovide an automata-theoretic characterization of regular MSC languages in terms of finite-state distributed automata called boundedmessage-passing automata. These automata consist of a set of sequential processes that communicate with each other by sending andreceiving messages over bounded FIFO channels. We also provide alogical characterization in terms of a natural monadic second-orderlogic interpreted over MSCs.A commonly used technique to generate a collection of MSCs isto use a Message Sequence Graph (MSG). We show that the class oflanguages arising from the so-called locally synchronized MSGs constitute a proper subclass of the languages which are regular in our sense.In fact, we characterize the locally synchronized MSG languages asthe subclass of regular MSC languages that are finitely generated