Regular collections of message sequence charts

Abstract. Message Sequence Charts (MSCs) are an attractive visual formalism used during the early stages of design in domains such as telecommunication software. A popular mechanism for generating a col-lection of MSCs is a Hierarchical Message Sequence Chart (HMSC). How-ever, not all HMSCs describe collections of MSCs that can be “realized” as a finite-state device. Our main goal is to pin down this notion of rea-lizability. We propose an independent notion of regularity for collections of MSCs and explore its basic properties. In particular, we characterize regular collections of MSCs in terms of finite-state distributed automata called bounded message-passing automata, in which a set of sequential processes communicate with each other asynchronously over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. It turns out that realizable collections of MSCs as specified by HMSCs constitute a strict subclass of the regular collections of MSCs.