Generalised Regular MSC Languages

Benedikt Bollig, Martin Leucker, Thomas Noll

We establish the concept of regularity for languages consisting of Message
Sequence Charts (MSCs). To this aim, we formalise their behaviour by
string languages and give a natural definition of regularity in terms of
an appropriate Nerode right congruence.  Moreover, we present a class
of accepting automata and establish several decidability and closure
properties of MSC languages. We also provide a logical characterisation
by a monadic second-order logic interpreted over MSCs. In contrast to
existing work on regular MSC languages, our approach is neither restricted
to a certain class of MSCs nor tailored to a fixed communication medium
(such as a FIFO channel).  It explicitly allows MSCs with message
overtaking and is thus applicable to a broad range of channel types like
mixtures of stacks and FIFOs.