Mechanisms for specifying and reasoning about collections of message sequence charts (MSCs) are addressed in this paper. MSCs are a helpful visual formalism used to capture system requirements during early design stages. The context here is telecommunications software, and the goal is to detect errors even at the requirements level.

The authors provide an automata-theoretic characterization of regular MSC languages that is given in terms of finite state distributed automata called bounded message-passing automata. Such automata constitute a set of sequential processes with communication that consists of sending and receiving messages over bounded first in-first out channels. Also provided is a logical characterization in terms of monadic second-order logic.

A common way to generate a set of MSCs is based on the use of hierarchical (high-level) MSCs (HMSCs). Message sequence graphs (MSGs) are HMSCs in which a node is labeled by an MSC. This paper provides a proof that shows that a regular MSC language can be represented by an MSG if and only if the language is finitely generated.

This paper will be of interest to researchers working on the theoretical aspects of distributed telecommunications software and its design.