B Adsul, M Mukund, K Narayan Kumar, Vasumathi Narayanan

*Proc. FSTTCS 2005*, Springer LNCS 3821 (2005) 335-347.

*© Springer-Verlag Berlin Heidelberg*

Message sequence charts (MSCs) are commonly used to specify interactions between agents in communicating systems. Their visual nature makes them attractive for describing scenarios, but also leads to ambiguities that can result in incomplete or inconsistent descriptions.

One problem that arises in this context is that of implied scenarios---a set of MSCs may imply new MSCs which are ``locally consistent'' with the given set. Alur, Etessami and Yannakis showed that if local consistency is defined in terms of local projections of actions along each process, it is undecidable whether a set of MSCs is closed with respect to implied scenarios, even for regular MSC languages.

We introduce a new and natural notion of local
consistency called *causal closure*, based on the
causal view of a process---all the information it collects,
directly or indirectly, through its actions. Our main result
is that checking whether a set of MSCs is closed with respect
to implied scenarios modulo causal closure is decidable for
regular MSC languages.

This decidability result yields an alternative definition
of *realizability* for MSC languages. It also allows
us to interpret MSC graphs modulo causal closure when
modelchecking properties, so that we can retain relatively
simple visual specifications without compromising on the
completeness and consistency of verification.

- Download PDF.