### Analysing Message Sequence Graph Specifications

Joy Chakraborty, Deepak D'Souza, K. Narayan Kumar

**IISc-CSA-TR-2009-1**

(March 2009) Available formats: [pdf]

Filed on March 17, 2009

Updated on May 14, 2009

We give a detailed construction of a finite-state transition

system for a com-connected Message Sequence Graph.

Though this result is fairly well-known in the literature there

has been no precise description of such a transition system.

Several analysis and verification problems concerning MSG

specifications can be solved using this transition system.

The transition system can be used to construct correct tools for

problems like model-checking and detecting implied scenarios in

MSG specifications.

The transition system we give can also be used for a bounded analysis

of general (not necessarily com-connected) MSG specifications.

Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2009/1/.Problems ? Contact techrep@csa.iisc.ernet.in

[Updated at 2009-10-22T06:42Z]