### Specification and verification using Message Sequence Charts

#### Anca Muscholl

LIAFA, case 7014
Université Paris-7

2 place Jussieu

75251 Paris Cedex 05, France

anca.muscholl@liafa.jussieu.fr
http://www.liafa.jussieu.fr/~anca/
#### Abstract

In this talk we present an overview of recent results on the use of Message
Sequence Charts (MSC) as a graphical specification formalism for communicating
distributed processes. We consider several questions concerning the expressivity
of the model and algorithmic verification of properties.

We first present the class of finite-state high-level MSCs, that exhibits
tight connections with Mazurkiewicz traces, [1]. For this class, Mukund et
al.[4] and very recently Kuske [1] showed the equivalence between definability
in monadic

second-order logic and acceptance by message passing automata.

In the second part we consider infinite-state high-level MSCs and the realizability
by message passing automata. We present subclasses of infinite-state high-level
MSCs that can be realized by such automata with or without deadlocks. These
results extend recent work of Alur et al. [1] and have been presented
at ICALP'02, [2].

#### References

[1] R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification
of MSC graphs. In:

*ICALP 2001*, LNCS

**2076**, pp. 797-808,
Springer 2001.

[2] B. Genest, A. Muscholl, H. Seidl and M. Zeitoun. Infinite-state High-Level
MSCs: Model-Checking and Realizability. In:

*ICALP 2002*, LNCS

**2380**
, pp. 657-668, Springer 2002.

[3] D. Kuske. A further step towards a theory of regular MSC languages. In:

*STACS 2002*, LNCS

**2285**, pp. 489-500, Springer 2002.

[4] M. Mukund, K. Narayan Kumar and M. Sohoni. Synthesizing distributed finite-state
systems from MSCs. In:

*CONCUR 2000*, LNCS

**1877**, pp. 521-535,
Springer 2000.