Abstracts for the LGTDS workshop

ICGT Conference , Barcelona, October 2002

Specification and verification using Message Sequence Charts

Anca Muscholl

LIAFA, case 7014
Université Paris-7
2 place Jussieu
75251 Paris Cedex 05, France


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].


[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.