Title: Deciding properties for message sequence charts

Authors: Anca Muscholl (1), Doron Peled (2), Zhendong Su (3)

(1) University of Stuttgart, Germany
(2) Bell Labs  and CMU, Pittsburgh,  USA
(3) University of California at Berkeley, USA

Abstract:

Message sequence charts (MSC) are commonly used in designing communication
systems. They allow describing the communication skeleton of a system
and can be used for finding design errors.  First, a specification
formalism that is based on MSC graphs, combining finite message
sequence charts, is presented.  We present then an automatic
validation algorithm for systems described using the message sequence
charts notation.  The validation problem is tightly related to a
natural language-theoretic problem over {\em semi-traces} (a
generalization of Mazurkiewicz traces, which represent partially
ordered executions).  We show that a similar and natural decision
problem is undecidable.