Extending Compositional Message Sequence Graphs


We extend the formal developments for message sequence charts (MSCs) to support scenarios with lost and found messages. We define a notion of extended compositional message sequence charts (ECMSCs) which subsumes the notion of compositional message sequence charts in expressive power but additionally allows to define lost and found messages explicitly. As usual, ECMSCs can be combined by means of choice and repetition to (extended) compositional message sequence graphs. We show that--despite extended expressive power--model checking of monadic second-order logic (MSO) for this framework remains to be decidable. The key technique to achieve our results is to use an extended notion for linearizations.

Download paper (Postscript)

BibTeX information

 author={Benedikt Bollig and Martin Leucker and Philipp Lucas},
 title={Extending Compositional Message Sequence Graphs},
 booktitle={Proceedings of the 9th International Conference on Logic for
  Programming, Artificial Intelligence and Reasoning (LPAR'02)},
 editor={Matthias Baaz and Andrei Voronkov},

back to publications

Valid XHTML 1.0 Strict, valid CSS.

Best viewed with any browser.

Author: Philipp Lucas.